Skip to content
Snippets Groups Projects
Select Git revision
  • 3d39850cb3645409ba4b7f5d499cd34f28c60559
  • develop default protected
  • jvm-ipc
  • master protected
  • 1.2.2
  • 1.2.1
  • 1.2.0
  • 1.1.0
  • 1.0.5
  • 1.0.4
  • 1.0.3
  • 1.0.2
  • 1.0.0
13 results

LTLError.mch

Blame
    • user avatar
    Sequences as relations
    hansen authored
    3d39850c
    History
    user avatar 3d39850c
    History
    Code owners
    Assign users and groups as approvers for specific file changes. Learn more.
    LTLError.mch 201 B 
    MACHINE LTLError
DEFINITIONS
ASSERT_LTL_1 == "F {x = 11}"
VARIABLES x
INVARIANT
 x : 1..10
INITIALISATION x:=1
OPERATIONS
  Inc = PRE x < 10 THEN x:= x + 1 END;
  Reset = PRE x = 10 THEN x := 1 END
END