-- Non-deterministic

MODULE main
    VAR
        state: 1..4;
    ASSIGN
        init(state) := 3;
        next(state) := case
            state = 1 : 2;
            state = 2 : 2;
            state = 3 : {1, 2, 4};
            state = 4 : 3;
        esac;

    DEFINE
        a := case
            state = 1 | state = 2 : FALSE;
            TRUE : TRUE;
        esac;
        
        b := case
            state = 1 | state = 3 : FALSE;
            TRUE : TRUE;
        esac;
    
    LTLSPEC F b; -- true
    LTLSPEC G a; -- false
    LTLSPEC a U b; -- false
    LTLSPEC a U X b; -- true
    LTLSPEC G F b; -- true
    LTLSPEC F G b; -- false

    LTLSPEC !(G a); -- false
    LTLSPEC !(a U b); -- false
    LTLSPEC !(F G b); -- false