https://sismic.readthedocs.io/en/latest/concurrent.html Maybe the concurrency factory. from sismic.io import import_from_yaml from sismic.interpreter import Interpreter satellite = Interpreter(import_from_yaml(filepath='satellite.yaml')) sendingstation = Interpreter(import_from_yaml(filepath='sendingstation.yaml')) missioncontrol = Interpreter(import_from_yaml(filepath='missioncontrol.yaml')) groundcontrol = Interpreter(import_from_yaml(filepath='groundcontrol.yaml')) satellite.bind(sendingstation) satellite.bind(missioncontrol) satellite.bind(groundcontrol) sendingstation.bind(satellite) sendingstation.bind(missioncontrol) sendingstation.bind(groundcontrol) missioncontrol.bind(satellite) missioncontrol.bind(sendingstation) missioncontrol.bind(groundstation) groundcontrol.bind(sendingstation) groundcontrol.bind(groundcontrol) groundcontrol.bind(missioncontrol) ==== satellite.yaml statechart: name: satellite preamble: resetlevel: -1 satelliteid: i description: | Satellites can fail by omission and up to f ground stations can fail traitorously. Mission Control is considered reliable though it will be checked. The basic transitions we will worry about will be a normal block being sent from multiple sending stations to a satellite, the satellite checking that it is legitimate for that slot and sending back an appropriate commit record. Thus, within the statechart, we can prove: (i) each satellite sends positive or negative commit records as it should and only for its slots (ii) each satellite updates lastpos and firstneg appropriately (iii) resets if accepted cause all slots to be partitioned among the satellites (so each slot will be handled by exactly one satellite) (iv) each Merkle Tree has been multi-signed by f+1 ground stations (v) each Commit Record has been multisigned by f+1 ground stations (vi) Mission control actions upon failure are correct and and the slot assignment partitions the slot space among satellites Then there can be a global invariant that asserts that there are no gaps among positive commit records in a reset set. So reset sequences will be well-formed. Outside of the statecharts, we will assert (i) the f failure and widespread knowledge assumptions and the clocks are more or less synchronized Outside of the statecharts, prove the lemmas already in the text. Initializing the satellite in state CommitNegative meaning satellite will refuse to commit any SendingStation message. root state: name: active parallel states: - name: missionControlListener initial: listeningMissionControl messageCollection := {} states: - name: listeningMissionControl transitions: - target: listeningMissionControl guard: validation of reset message succeeds action: | initialize flags set reset level set slot schedule set signatures of reliable sending stations set signatures of reliable ground stations set firstneg to undefined satellitestatus := True send(positive ConfirmReset) - target: listeningMissionControl guard: validation of reset message fails action: | satellitestatus := False send(negative ConfirmReset) - name: clockListener initial: listeningClock - name: listeningClock transitions: - target: handleSlot guard: a slot for this satellite arrives and satellitestatus action: | choose one well-formed SendingStation message from messageCollection - name: handleSlot - target: listeningClock guard: slot ends and (validation of Sending Station Message fails or no Sending Station Message received at slot) and firstneg is undefined action: | messageCollection:= {} firstneg := current reset level and current slot satellitestatus := False send(negative CommitRecord) - target: listeningClock guard: slot ends and firstneg is defined action: | messageCollection:= {} send(negative CommitRecord) - target: listeningClock guard: slot ends and (validation of Sending Station Message succeeds) and firstneg is undefined action: | messageCollection:= {} lastpos := current reset level and current slot send(positive CommitRecord) - name: sendingStationListener initial: listeningSendingStation - name: listeningSendingStation - target: listeningSendingStation guard: Sending Station Message is for a slot that isn't over and isn't being processed action: | messageCollection += SendingStationMessage ===== sendingstation.yaml statechart: name: sendingStation preamble: resetlevel: -1 description: | Once Sending Stations receive resets from Mission Control and confirmation of ConfirmResets from all the satellites in the Reset, the Sending Stations can begin operation. They assemble a block, send the Merkle Tree around, wait for a multisigned response, wait for multisigned CommitRecord of previous block or the reset message. Let's see: start off in a state waiting for a first reset. Once a reset is received, then enter a state of waiting for positive confirm resets. Once all set, then Sending Station starts to formulate blocks for appropriate slots. root state: name: satelliteListener sendingstationstatus:= False satelliteSet := {} parallel states: - name: satelliteListener states: - name: gatherMessages transitions: - target: gatherMessages guard: validation of ConfirmReset from one satellite j and satelliteSet != set of satellites in slot partition of ConfirmReset and sendingstationstatus == False action: | insert j into SatelliteSet - target: satelliteListener guard: validation of ConfirmReset from satellite j and sendingstationstatus == False and satelliteSet == set of satellites in slot partition of ConfirmReset and all ConfirmResets received for this reset level are consistent in slot partition, reset number, valid ground stations, valid Sending Stations ... action: | record slot schedule record reset number from ConfirmReset record valid ground stations and their public keys sendingstationstatus := True satelliteSet := {} - target: satelliteListener guard: validation of ConfirmReset fails and sendingstationstatus == False action: | send(message to Mission Control) - name: clockListener transitions: - target: clockListener guard: sendingstationstatus == True and clock indicates this slot i reset r, slot i for me action: | send(request multisigned commit for reset r, slot i-1 to Ground stations) prepare block and MerkleTree send(request multisigned root of this MerkleTree to Ground stations) - name: groundStationListener transitions: - target: groundStationListener guard: sendingstationstatus == True and in reset r, slot i and reset r, slot i is one of my slots and have proper multisigned positive commit record for reset r, slot i-1 and multisigned root for Merkle Tree that I have produced for reset r, slot i action: | assemble message for reset r, slot i send(SendingStation message for reset r, slot i to satellite for this slot) - target: groundStationListener guard: sendingstationstatus == True and in reset r, slot i and reset r, slot i is one of my slots and negative commit record for reset r, slot i-1 action: | sendingstationstatus := False send(Alert Mission Control that there is a negative Commit Record) ===== missioncontrol.yaml statechart: name: missionControl preamble: resetlevel: -1 description: | Mission control at initialization or after some times, sees that a sending station protests because it receives a negative commit record or Mission Control simply sees that no progress is being made. Mission Control then issues a reset to the satellites. Satellites send confirmResets in response. root state: name: startstate transitions: - target: allQuiet guard: signal to start and reset level == -1 form ResetMessage with reset level set to 0 and slot assignment and public keys of valid ground stations and sending stations send(ResetMessage) parallel states: - name: sendingStationListener states: - name: allQuietSending transitions: - target: allQuietSending guard: receive negative Commit Record from Sending Station with current reset level action: | missionControlStatus:= startReset send(RequestStatus to satellites) lastposrecorded = -infinity lastnegrecorded = +infinity - name: satelliteListener states: - name: receivingModeSatellite transitions: - target: receivingModeSatellite guard: received response to RequestStatus and not true that firstneg = lastpos + 1 all with previous reset level action: | lastposrecorded = max( lastposrecorded, lastpos from RequestStatus) firstnegrecorded = min(firstnegrecorded, firstneg from RequestStatus) - target: consultGroundStations guard: (significant time has passed since RequestStatus and not true that firstnegrecorded = lastposrecorded + 1 all with previous reset level) or (have heard from all satellites and not true that firstnegrecorded = lastposrecorded + 1 all with previous reset level) action: | ask ground stations to see which commit records they know for current reset level between slots lastposrecorded and firstnegrecorded - target: formReset guard: received response to RequestStatus and firstnegrecorded = lastposrecorded + 1 all with previous reset level action: | form ResetMessage with next reset level and new slot assignment and public keys of valid ground stations and sending stations send(ResetMessage to satellites) - name: groundStationListener states: - name: receivingMode transitions: - target: receivingMode guard: have received from Ground Stations commit records such that the least slot number n for a negative commit record for this reset level r and the maximum slot number p for a positive commit record for reset level r have the property that n = p+1 action: | form ResetMessage with next reset level and new slot assignment and public keys of valid ground stations and sending stations send(ResetMessage to satellites) ===== groundstation.yaml statechart: name: groundStation preamble: description: | Ground stations receive commit records from satellites which they spread and multisign, receive messages from Sending Stations from which they assemble Merkle Roots and gossip and then multisign. root state: name: startstate transitions: - target: allQuietSatellite guard: signal to start parallel states: - name: satelliteListener states: - name: allQuietSatellite transitions: - target: allQuietSatellite guard: ConfirmReset message from satellite action: | send(ConfirmReset) to other ground stations and end users to make it widespread - target: gossippingModeSatellite guard: CommitRecord message for some reset r slot i from satellite action: | Gossip with at least f+1 other Ground Stations to form a multisignature of Commit - name: gossippingModeSatellite transitions: - target: allQuietSatellite guard: have received a multisigned commit record of some reset r slot i - name: sendingStationListener states: - name: allQuietSending transitions: - target: gossippingModeSending guard: receive Merkle Tree T for slot i from Sending Station action: | form Merkle root of T send both T and signed Merkle root of T to at least f+1 other Ground Stations to form a multisignature of Merkle root of T merklerootmulti:= {} - name: allQuietSending transitions: - target: allQuietSending guard: receive request from Sending Station for Commit Record of some reset r slot i-1 and that multisigned Commit Record is available action: | send multisigned Commit Record of reset r slot i-1 to Sending Station - name: allQuietSending transitions: - target: allQuiet guard: receive request for Merkle root of some reset r slot i and merklerootmulti is defined and pertains to this reset level and this slot action: | send merklerootmulti to Sending Station - name: groundStationListener states: - name: allQuietGround transitions: - target: allQuietGround guard: receive Merkle Tree T for slot i and signed Merkle root of T action: | myroot:= form Merkle root of T if received Merkle root == myroot then multisign received Merkle root send back to ground station from which T came - target: allQuietGround guard: receive multisigned Merkle root of T by at least f+1 Ground Stations and that root corresponds to the root this Ground Station calculated action: | merklerootmulti:= multisigned Merkle root of T - name: missionControlListener states: - name: allQuietMission transitions: - target: allQuietMission guard: receive request from Mission Control for greatest slot number of a positive commit record for current reset level r and least slot number of a negative ommit record for current reset level r action: | see what this ground station has recorded and send back the relevant Commit Records