Contract as a state machine (states and transitions)
When possible, defining a contract as a state machine is very convenient because it makes it simpler to:
get an insight in the global contract mechanism (easier to read and understand)
formally verify the contract properties (more assumptions can be done on a state)
States
It is possible in Archetype to define a global contract state . The following example creates 5 states:
1
states =
2
|Created initial
3
|Confirmed
4
|Completed
5
|Aborted
6
|Canceled
Copied!
initial is a keyword to set the default state.
When necessary, action effects may read the state value (but cannot change it), as in the example below:
1
effect {
2
...
3
match state with
4
|Created-> fail ("cannot do that in Created state")
5
end;
6
...
7
}
Copied!
Transitions
Transitions are necessary to change the state of the contract. For example the following snippet declares the transition confirm to go from Created to Confirmed:
1
transition confirm (){
2
from Created
3
toConfirmed
4
with effect {
5
...(* after this, state is set to Created *)
6
}
7
}
Copied!
Like actions, transitions may have arguments, and also have the called byspecification and require sections.
It is also possible to decide the resulting state. For example the following decide transition determine the resulting state based on a condition <COND> :
1
transition mayconfirm (){
2
from Created
3
toConfirmedwhen{<COND>}
4
with effect {
5
...(* after this, state is set to Created *)
6
}
7
8
toCanceled(* execute this when <COND> is false *)
9
with effect {
10
...(* after this, state is set to Canceled *)
11
}
12
}
Copied!
Example
Follow the link below to observe the basic escrow example implemented as a state machine.