test.ref

type XYZ: struct {
    a: integer;
    b: number;
};

type ABC: struct {
    a: integer;
    b: number;
    c: boolean;
    d: struct {
        x: integer;
    };
    x: XYZ[1][2];
    z: integer[7][6];
};


conf xyz: XYZ;

data abc: ABC;
data alpha: boolean;
data beta: boolean;
data plain: integer;

#abc.a == 456;
xyz.a == 0x12345678;
xyz.b == 1.2;

#Us(__time__ < 5, __time__ == 5);
#Uw(__time__ < 5, __time__ == 5);
#Xs(abc.a == 123);
#Xw(abc.a == 567);
#abc.a == 456;

#Xs(Us[abc.a + 123:abc.a + 345](abc.a == 2, abc.a == 3));
#Xw(Us[abc.a + 123:abc.a + 345](abc.a == 2, abc.a == 3));
#Xs(Uw[abc.a + 123:abc.a + 345](abc.a == 2, abc.a == 3));
#Xw(Uw[abc.a + 123:abc.a + 345](abc.a == 2, abc.a == 3));

#Xs(Us[abc.a + 123:abc.a + 345](abc.a == 2, abc.a == 3));
#Us[abc.a + 123:abc.a + 345](abc.a == 2, abc.a == 3);
#Us[abc.a + 123:abc.a + 345](abc.a == 2, abc.a == 3);

#starting@(Us(starting.abc.a == 1234, abc.x[1][1].a == 3));

#F(abc.a == 2);
#abc.a + 12 == 2;
#abc.d.x == 1;
#__time__ == 1;
#plain == 3;

#abc.x[2][3].a == 3;
#abc.z[2][3] == 2;

#x@(x.abc.a != 2);

#G(((true)));
#F(2 == abc.a);
#F(false == abc.c);
#Us(alpha, abc.a != abc.b);
#Us[1:3](alpha, beta);
#Rw[1:3](alpha, beta);

#G(x@(x.abc.a == 3));
#G(x@(xyz.a == 3));

type Button:    enum {DEPRESSED, RELEASED};
type State:     enum {ON, OFF};
type Door:      enum {OPENED, CLOSED};

data button:    Button;
data lock:      State;
data alarm:     State;
data door:      Door;

#F(button.DEPRESSED);
#button.DEPRESSED;

before button.DEPRESSED, lock.ON eventually holds after 100 milliseconds;   
globally, it is never the case that door.CLOSED && alarm.ON;    
while door.OPEN, it is always the case that alarm.ON after 30 seconds;  
globally, if button.DEPRESSED, then in response lock.ON after 100 milliseconds;
globally, once lock.ON becomes satisfied it remains so for at least 2 seconds;    
globally, once lock.ON becomes satisfied it remains so for less than 2.2 seconds; 
between door.CLOSED and lock.OFF, it is always the case that door.CLOSED;   
after lock.ON, if door.OPEN, then it must have been the case that lock.OFF has occurred before it; 
after lock.ON, if lock.OFF, then it must have been the case that button.DEPRESSED has occurred before;