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)
It is possible in Archetype to define a global contract state . The following example creates 5 states:
states =| Created initial| Confirmed| Completed| Aborted| Canceled
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:
effect {...match state with| Created -> fail ("cannot do that in Created state")end;...}
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
:
transition confirm () {from Createdto Confirmedwith effect {... (* after this, state is set to Created *)}}
Like actions, transitions may have arguments, and also have the called by
specification
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>
:
transition mayconfirm () {from Createdto Confirmed when {<COND>}with effect {... (* after this, state is set to Created *)}to Canceled (* execute this when <COND> is false *)with effect {... (* after this, state is set to Canceled *)}}
Follow the link below to observe the basic escrow example implemented as a state machine.