State machines are incompatible with concurrent systems. For example there is no nondeterministic state machine for the following program: IndeterminateLar

State machines are incompatible with concurrent systems. For example there is no nondeterministic state machine for the following program: IndeterminateLargeNumber:[]→Natural ≡ []↦ aCounting←Counting.[], // Bind aCounting to a newly created Counting aCounting.go||| // Send aCounting a go message while concurrently aCounting.stop // sending aCounting a stop message Counting:[ ]→Interface go→Void, stop→Natural ≡ [] ↦↦ // constructor has no arguments count:=0, // The variable count is initially 0 continue:=False| // The variable continue is initially False go ↦ // When a go message is received: continue cases // Cases for continue are as follows: True then // If continue is True, count:=count+1; // then increment count and afterward Hole (This Counting).go // in a hole in the region of mutual exclusion, send a go message this instance of Counting else Void // If continue is False, then return Void stop ↦ // When a stop message is received: continue:=False; // Assign continue the value False and then count // return the value of count See the following for an explanation: https://papers.ssrn.com/abstract=3459566 https://papers.ssrn.com/abstract=3459566