Skip to content
Snippets Groups Projects
Commit 652e8709 authored by Fabian Vu's avatar Fabian Vu
Browse files

Try to fix a few tests

parent a393e2e2
No related branches found
No related tags found
No related merge requests found
Pipeline #149367 failed
MACHINE Assert
VARIABLES floor
VARIABLES level
INVARIANT floor : 0..99 /* NAT */
INVARIANT level : 0..99 /* NAT */
INITIALISATION floor := 0
INITIALISATION level := 0
OPERATIONS
inc = ASSERT floor<99 THEN floor := floor + 1 END ;
inc = ASSERT level<99 THEN level := level + 1 END ;
dec = ASSERT floor>0 THEN floor := floor - 1 END
dec = ASSERT level>0 THEN level := level - 1 END
END
\ No newline at end of file
MACHINE Lift
VARIABLES floor
VARIABLES level
INVARIANT floor : 0..100 /* NAT */
INVARIANT level : 0..100 /* NAT */
INITIALISATION floor := 0
INITIALISATION level := 0
OPERATIONS
inc = PRE floor<100 THEN floor := floor + 1 END ;
inc = PRE level<100 THEN level := level + 1 END ;
dec = PRE floor>0 THEN floor := floor - 1 END
dec = PRE level>0 THEN level := level - 1 END
END
\ No newline at end of file
MACHINE Lift_External
VARIABLES floor
VARIABLES level
INVARIANT floor : 0..100 /* NAT */
INVARIANT level : 0..100 /* NAT */
INITIALISATION floor := 0
INITIALISATION level := 0
OPERATIONS
inc = PRE floor<100 THEN floor := floor + 1 END ;
dec = PRE floor>0 THEN floor := floor - 1 END;
inc = PRE level<100 THEN level := level + 1 END ;
dec = PRE level>0 THEN level := level - 1 END;
EXTERNAL_SEND = skip
END
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment