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
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102

------------------------------ MODULE IndicesExec ------------------------------
\* This is the model of Substrate Frame Indices from 
\* https://github.com/paritytech/substrate/tree/master/frame/indices 
\* at this commit: https://git.io/Ju5Jv
\*\*
\* This is the execution environment for the Indices.tla model.
\*
\* This TLA+ model is created for demostrative purposes of MBT capabilities.
\* 2021 Andrey Kuprianov, Informal Systems

EXTENDS Indices


\* Actions: boilerplate code that checks preconditions, executes updates,
\* and stores action and actionOutcome.
\* This code will be auto-generated in the next versions of Modelator.

ClaimAction ==
  \E who \in Addresses:
  \E index \in Indices:
    /\ action' = [ type |-> "Claim", who |-> who, index |-> index ]
    /\ LET outcome == ClaimOutcome(who, index) IN 
        actionOutcome' = outcome /\
        IF outcome = OK THEN
          Claim(who, index)
        ELSE
          UNCHANGED <<indices, reserved>>

TransferAction ==
  \E who, new \in Addresses:
  \E index \in Indices:
    /\ action' = [ type |-> "Transfer", who |-> who, new |-> new, index |-> index ]
    /\ LET outcome == TransferOutcome(who, new, index) IN 
        actionOutcome' = outcome /\
        IF outcome = OK THEN
          Transfer(who, new, index)
        ELSE
          UNCHANGED <<indices, reserved>>

FreeAction ==
  \E who \in Addresses:
  \E index \in Indices:
    /\ action' = [ type |-> "Free", who |-> who, index |-> index ]
    /\ LET outcome == FreeOutcome(who, index) IN 
        actionOutcome' = outcome /\
        IF outcome = OK THEN
          Free(who, index)
        ELSE
          UNCHANGED <<indices, reserved>>

ForceTransferAction ==
  \E who, new \in Addresses:
  \E index \in Indices:
  \E freeze \in BOOLEAN:
    /\ action' = [ type |-> "ForceTransfer", who |-> who, new |-> new, index |-> index, freeze |-> freeze ]
    /\ LET outcome == ForceTransferOutcome(who, new, index, freeze) IN 
        actionOutcome' = outcome /\
        IF outcome = OK THEN
          ForceTransfer(who, new, index, freeze)
        ELSE
          UNCHANGED <<indices, reserved>>


FreezeAction ==
  \E who \in Addresses:
  \E index \in Indices:
    /\ action' = [ type |-> "Freeze", who |-> who, index |-> index ]
    /\ LET outcome == FreezeOutcome(who, index) IN 
        actionOutcome' = outcome /\
        IF outcome = OK THEN
          Freeze(who, index)
        ELSE
          UNCHANGED <<indices, reserved>>


Next == 
  \/ ClaimAction
  \/ TransferAction
  \/ FreeAction
  \/ ForceTransferAction
  \/ FreezeAction


\* Auxiliary operators

TakenIndices == { i \in DOMAIN indices : indices[i].who /= None }

\* Is it an invariant?

IndexRequiresReserve ==
  \A index \in TakenIndices:
    reserved[indices[index].who] /= 0


\* Negate the above to get the test
TestIndexWithoutReserve ==
  \E index \in TakenIndices:
    reserved[indices[index].who] = 0

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