modelator 0.4.2

A framework and tools for model-based testing.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30

------------------------------------ MODULE 2PossibleTraces -----------------------------
(*
There should be only two possible paths for x to reach 3
0 -> 1 -> 3
0 -> 2 -> 3
*)

EXTENDS Integers, FiniteSets, Sequences, TLC

VARIABLES 
    \* @type: Int; 
    x

\* @type: () => Bool;
Init == x = 0

ZeroToOne == x = 0 /\ x' = 1
ZeroToTwo == x = 0 /\ x' = 2
OneToThree == x = 1 /\ x' = 3
TwoToThree == x = 2 /\ x' = 3
ThreePlus == 2 < x /\ x' = x + 1

Next == 
    \/ ZeroToOne
    \/ ZeroToTwo
    \/ OneToThree
    \/ TwoToThree
    \/ ThreePlus

===============================================================================