Proposal: BFT protocol that can mutate its operator set in a byzantine setting

Michal · December 16, 2023, 8:31pm

Task

Identify a BFT protocol that can mutate its operator set in a byzantine setting. In other words describe DV cluster states and transitions – allow the Obol operator’s cluster to add and remove operators, efficiently start and exit validators or stop the cluster.

Background

Obol Charon’s framework was built around a lock file, which defined the state of system participants. This static setup has been effective in the past. However, we now face the challenge of adapting this system to allow for flexible modifications to the cluster without causing disruptions to the ongoing operations.

Problem Statement

In Obol, we group sets of participants into clusters. Their stability and efficiency are paramount. A significant challenge in such a setting is managing the dynamic state of the DV cluster hosted on top of Byzantine Fault Tolerant (BFT) protocols. How do we keep the system state moving while performing operations requiring a complicated setup? How do we allow new members to join and leave while clearly understanding the DV state?

So the Problem Statement is to describe cluster communication rules as well as the cluster state model so that the DV cluster would behave predictably and never lock concerning given constrains (here by “lock” we mean cases when required operations order gets confused due to operator disagreement or operations ordering issues).

Challenges

BFT does not save individual nodes from dis-coordination - multiple nodes can try to propose different mutations to be initiated. E.g., we started adding a validator and suddenly understood we needed to ban an operator as it is not responsive due to our state model. Thus, this document aims to cover “no going back when started” composite mutation attacks by nodes breaking the mutation sequence rules and halting cluster state progression, meanwhile changing the set of operators leading to the mutation having to be dropped altogether.
Initial Obol research on this topic assumes that some of the state changes can be done by individual operator signing. This can lead to a single node gaining the ability to halt a cluster. Thus we will investigate such halting and possible state change rules that can prevent cluster halting. This is different from (1) in the way that an attack here is a willing full-actor action on an ongoing composite mutation.
Current obol research on potential system state changes needs to define exit strategies for validators, operators, and clusters. This means that currently, the only mechanism for operator exit is an Operator Ban that removes system potential for clear consensual node exit and can, in the future, lead to the system’s inability to impose and distinguish bad actors from good ones.

Proposed solution

State model

We expend Obol state model from Obol Design Doc that already uses composite mutations to support cluster exit, validator stopping:

Consensus game rules:

We add the following rules to respect the nature of synchronised distributed state changes:

There shall be only one of each composite mutation type running in parallel. Each running composite mutation shall have its timestamp+UUID (unique id for cluster definition) synchronised across the operator set. A particular implementation may use other composite mutation tracking against the distributed state over time logic, here only the principal idea of knowing all running composite mutation types matters.
Any successful composite mutation (one that has enough signatures on each mutation it is composed of and has no invalidation or cancelling mutation happening) of the operator set cancels and declines all other running mutations (for example, by timestamp+UUID providing a cut off on the DAG).

As in BFT, there is always a leader proposing the state update. We assume that mutations that are single-user state updates can be

Provided by the node when it becomes a leader. Here, we assume BFT implementation to be reliable for state agreement and consistency between nodes, with the leader receiving information on if his proposal was not agreed to (due to time frame or quorum disagreement).
Or sent to a leader as a request if selected BFT flavour or other architectural challenges make it hard for a node to be a leader.

For an external observer, these composite mutation state-changing mechanisms can look like a set of operations, each running in a loop, yet as we allow only one composite mutation of each type at the same time, the resulting system state changes are:

Easily manageable, one can always
1. view all currently running mutations,
2. update operators set via banning or voluntary exit in parallel with other running mutations,
3. cancel outdated running mutations if needed by submitting new mutation that is part of a composite mutation of the same type making previous composite mutation irrelevant (as we have only up to one composite mutation type running at the same time).
State evolution can be easily stored in external monitoring solutions and tracked over time in a nearly linear fashion

Model formal verification

We test the proposed model, recreating it using the formalism of the Petri network (PN) model with inhibitor arcs. To allow needed complexity, we devise a set of PN component blocks that we later interconnect together where each one can be verified separately for reachability and lockability. (described in Appendix A).

Each composable mutation can be defined similarly to this “Change Operators” one:

And simplified into a set of main actions:

Overall system model as a Distributed System state machine modeled from PN components (notation as on the figures above):

Here we can change validators and operators set; have validators enabled or disabled, stop cluster gently after exiting all validators.

Model was described in .net format verifiable by common PN verification tools an was verified and tested using opensource SMPT tool (which ”won a bronze medal in the “reachability” category of the Model Checking Contest 2022, an international competition of model checking tools for the verification of concurrent systems. It also obtains the 100% confidence award.”).

Resulting state model addressing certain aspects, such as the consensual removal of nodes looks like this (on top level each state is a result of one or more mutations):

Action \ Requirements	All/Quorum/Single Affirm	Description
Create cluster	all	Setting up a new DV cluster. Every member or entity that will be part of this cluster needs to participate or consent to its creation.
Change operators	quorum old, all new	altering the set of operators who have the authority to manage and control the cluster
Add validators	all	Register validator within operators set for control and duties performance
Stop Validator	quorum	Exit validator
Update/Add cluster metadata	quorum	Modifying or adding new information to the cluster’s metadata, such as configuration details
Update/Add operator metadata	single	Operators can update their own metadata, such as contact details or specific settings
Rotate node identity	quorum	Changing a node’s identity, like updating cryptographic credentials
Cluster Exit	quorum	This process ensures orderly and consensual disbanding or restructuring of the cluster.

Note that a quorum of operators generates deposit data, and the principal provider activates the validator using this deposit data so in real life this happens out of the scope of BFT consensus state while here we add or remove validators to operators within our model.

Drawbacks of the proposed solutions:

Also as some of the decisions happen off-chain there is a potential for deadlocks caused by issues of quorum aggregation (as some synchronization happens in the background in off-chain channels as described in the Task statement). This can especially arise on every action that requires “All” to sign instead of “Quorum”, note that in some of the actions, we should assume only Quorum and newer be able to check for “All”. Thus a recommendation can be made to demote operations currently set requiring all nodes to synchronise to only the quorum subset, or use only BFT implementations where a check for All to consent is available.

State model can not provide additional guarantees on top of those provided by the general application of the BFT+DAG consensus algorithm utilized underneath in terms of resistance to Byzantine nodes.

Created model assumes state model is eventually consistent and messages are delivered in uncorrupted form.

Results:

In the presented model, we:

Proposed solution for banning an operator when a composed mutation has started
Introduced rules allowing to control of individual operators signing state-updating mutations
Defined exit strategies for the state model

We have a formalised, generalized model of BFT Consensus-based State Change using Petri Networks

We can now model readability and deadlock for a wide set of system flow graphs based on BFT consenting (or declining nodes)

We gathered a complete states graph model including Validators and Operators Exiting and Cluster termination

Appendix A: Components of Petri Network

We want to be able to model this solution as a Formal model. Thus we developed a conceptual framework and code for the generation of our network description in Petri Networks with inhibitor arcs .net language. We consider the implementation of:

Composite mutations (with up to one of each type running concurrently)
Set of Operators that elect a leader and who create a decision of what operation to partake in (DV BFT cluster)
A set of Validators that can be considered activated or deactivated during the DV cluster runtime by moving them into Active Validators set

As Petri Networks contain only:

marks
places
transitions
arcs

we need to expand this set with components that would scale automatically and implement parts needed for the task such as Set, Act, Vote by Quorum, Update State.

Set

Most work in our model revolves around Set mutations
Add item

Remove item

Emptiness check

Set Items counting

We then generalise Set component description (where N is max set capacity we allow in out model):

This allowed us to instantiate as many sets as we want using short code listings like

And display them in Formal Verification Application:

We introduce petri network model that includes dynamic network capacity and max occupancy

Schematic depiction of action in presence of disabled nodes

We replicate this structure for all possible Nodes composition

This all lead us to a notion of Consensus decision process that looks like this:

We generate quorum checker for k of N nodes (here N is the number of nodes in the cluster and k is the quorum)
If we set k = N we can check that all nodes voted

Schematic depiction of a node selecting an Activate decision

Each node can make a set of possible action choices

Schematic depiction of state action selection

Next we want to model how consensus can be shown in the presence of many nodes and possible actions in details

Modelling BFT Consensus-based State Change using Petri Networks

In BFT we always have a leader-like node

Leading node proposes action (state change, this is all done by underlying BFT including state sync details of which are out of our current scope)

others verify (\operatorname{Quorum}(k) nodes)

System updates state

Schematic depiction of Composite mutations leading to system state update

Leader Election ( for the first nodes in the node-set we highlight in green the action path that could happen, and in red, dependencies of each action associated with a corresponding PN model transition)

Leader Action flow

Quorum on Leader Action (here for clarification of the action result, we highlight the decision reached/cancelled in green and red, and the PN place where the token may be placed for forced task cancellation in yellow)

Frame-based Node Action Start

Pruning based clean up on Quorum end

Updated Schematic action flow

Updated Quorum on Leader Action

Using the fact that PNs are deterministic we can split yes/no decisions and remove Time Frame End dependency from here

Multistage mutations correlation

Modeling Quorum Consensus using Petri Networks

Our state is governed by composite mutations thus a single System state update can look like this:

this example depicts our most complicated composite mutation, all others work in similar fashion

to simplify its future representation we will use such Composite Mutation System state update type simplified depictions:

We can cancel, start, lock on the process and check for success of ending of any composite mutation.

And thus overall system model would look like such Distributed System state machine:

Untitled

Here we can change validators, operators set; have validators enabled or disabled, stop cluster gently after exiting all validators.

Appendix B: Petri Network Code generator

To facilitate standartised network generation we developed the following components:

Place class:
- __init__(self, name, marking=0): Initializes a place with given a name and initial marking (i.e., token count).
- __str__(self): Returns the human-readable string representation of the place.
- Public Variables: name (name of the place), marking (current token count of the place).
Transition class:
- __init__(self, name): Initializes a transition with a given name.
- From(self, place, weight=1): Specifies a place (and its token weight) from which tokens are consumed when the transition fires.
- To(self, place, weight=1): Specifies a place (and its token weight) to which tokens are produced when the transition fires.
- add_inhibitor_arc(self, place, weight=1): Adds an “inhibitor arc”, i.e., a condition that must be satisfied for a transition to fire; specifically, the associated place cannot have more than a certain number of tokens (weight).
- __str__(self): Returns the human-readable string representation of the transition.
- Public Variables: name (the name of the transition), from_places (list of places from which tokens are taken), to_places (list of places to which tokens are added), inhibitor_arcs (list of places that inhibit the firing of the transition if they have more than a given weight of tokens).
SubSystem class:
- __init__(self, model): Initializes a subsystem within a given model.
- add_place(self, place): Adds a place to the subsystem.
- add_transition(self, transition): Adds a transition to the subsystem.
- wire_up(self): Stub method for wiring up the places and transitions within the subsystem (implementation depends on the specific subsystem).
- Public Variables: model (the encompassing model), places (list of places in the subsystem), transitions (list of transitions in the subsystem).
ConstSizeSetSubSystem class (extends SubSystem):
- __init__(self, model, name, N): Initializes a subsystem with a given model, name, and size N.
- Public Variables: N (size of set), name (name of the subsystem), set_places (list of places representing set), add_item_place (place for adding items), remove_item_place (place for removing items), set_items_counter_place (place for counting items in the set), empty_check_transition (transition for checking if set is empty), add_to_set_transitions (list of transitions for adding to set), remove_from_set_transitions (list of transitions for removing from set).
LeaderElection class (extends SubSystem):
- __init__(self, name, set_system): Initializes a LeaderElection subsystem with a given name and set system.
- Public Variables: name (name of the subsystem), set_system (the associated set system), selected_place (place representing the selected leader), processed_place (place representing the processing state of the system), selection_transitions (list of transitions for leader selection), round_transition (transition representing a round of leader election), release_transitions (list of transitions for releasing non-leader nodes).
LeaderVoteLock class (extends SubSystem):
- __init__(self, name, leader_election): Initializes a LeaderVoteLock subsystem with a given name and associated LeaderElection system.
- Public Variables: name (name of the subsystem), leader_election (the associated leader election system), action_begins_place (place indicating beginning of action), action_is_running_place (place indicating action is still running), action_begins_transaction (transition representing the beginning of an action), action_got_decision_place (place representing a decision has been made), round_ends_transition (transition representing the end of a round).
1. VoteOnLeaderAction class (extends SubSystem):
  - __init__(self, name, lock, voters): Initializes a VoteOnLeaderAction subsystem with a given name, associated LeaderVoteLock (lock), and a set of voters.
  - Public Variables: name (name of the subsystem), lock (the associated LeaderVoteLock system), voters (the set of voters system), on_frame_transition (transition represents an event frame), on_frame_begins_places (list of places that tracks when an event frame begins for each voter), active_places (list of places indicating the active voting state for each voter), node_activation_transitions (list of transitions for activating voters), action_accepted_places (list of places indicating where each voter accepts the action), action_declined_places (list of places indicating where each voter declines the action), act_yes_transitions (list of transitions for acceptances), act_no_transitions (list of transitions for declinations).
2. VotesQuorumCheckerAction class (extends SubSystem):
  - __init__(self, percentage, name, nodes_votes, check_accepted): Initializes a VotesQuorumCheckerAction subsystem with a given percentage (for quorum checking), name, associated VoteOnLeaderAction (nodes_votes), and a flag to specify whether to check for acceptance (check_accepted).
  - Public Variables: percentage (quorum percentage), name (name of the subsystem), nodes_votes (the associated VoteOnLeaderAction system), votes_place (place accumulating votes), quorum_place (place indicating whether quorum was reached), prune_place (place initiating the prune operation), pruned_place (place indicating pruning has occurred), consensus_reached_place (place indicating if consensus was reached).
3. CompositeMutation class (extends SubSystem):
  - __init__(self, model, name, states): Initializes a CompositeMutation subsystem with a given model, name, and possible states of mutation.
  - Public Variables: name (name of the subsystem), states (possible states of mutation), place_next, place_operation_canceled, place_processing, place_on_declined, place_on_success (places indicating the various stages of mutation operation) , transition_got_canceled, transition_got_finished, places_on_mutation, transitions_got_mutation, transitions_declined (transitions indicating operation cancellations, mutation progress, and possible declines).
4. FramedSystem class (extends SubSystem):
  - __init__(self, model, name, operators_set, possible_mutations, mutations_states, consensus_accept_percentage=66.6): Initializes a FramedSystem subsystem with a given model, name, set of operators, possible mutations, possible mutation states, and a consensus accept percentage.
  - Public Variables: name (name of the subsystem), model (the encompassing model), possible_mutations (list of possible mutation states), nodes_set, leader_election_system, leader_vote_lock, vote_action, vote_checker_accepted, vote_checker_declined, composite_mutations (various subsystems and classes for managing the operators, leader elections, votes, vote checking, and handling mutations).
- And their implementations allowing us to model and verify system described in Appendix A:
```
class Place:
    def __init__(self, name, marking=0):
        self.name = name
        self.marking = marking

    def __str__(self):
        return f"pl {self.name} ({self.marking})"

class Transition:
    def __init__(self, name):
        self.name = name
        self.from_places = []
        self.to_places = []
        self.inhibitor_arcs = []

    def From(self, place, weight=1):
        self.from_places.append((place, weight))

    def To(self, place, weight=1):
        self.to_places.append((place, weight))

    def add_inhibitor_arc(self, place, weight=1):
        self.inhibitor_arcs.append((place, weight))

    def __str__(self):
        inputs = " ".join([f"{place.name}?-{weight}" for place, weight in self.inhibitor_arcs])
        inputs += " " + " ".join([f"{place.name}*{weight}" for place, weight in self.from_places])
        outputs = " ".join([f"{place.name}*{weight}" for place, weight in self.to_places])
        return f"tr {{{self.name}}} {inputs.strip()} -> {outputs.strip()}"

class SubSystem:
    def __init__(self, model):
        self.model = model

        self.places = []
        self.transitions = []

    def add_place(self, place):
        self.places.append(place)
        self.model.add_place(place)

    def add_transition(self, transition):
        self.transitions.append(transition)
        self.model.add_transition(transition)

    def wire_up(self):
        pass

class Model:
    def __init__(self):
        self.subsystems = []
        self.places = []
        self.transitions = []

    def add_subsystem(self, subsystem):
        self.subsystems.append(subsystem)

    def add_place(self, place):
        self.places.append(place)

    def add_transition(self, transition):
        self.transitions.append(transition)

    def print_network(self):
        for subsystem in self.subsystems:
            subsystem.wire_up()
        for place in self.places:
            print(place)
        for transition in self.transitions:
            print(transition)
        print("net buffer")

class ConstSizeSetSubSystem(SubSystem):
    def __init__(self, model, name, N):
        super().__init__(model)
        self.N = N
        self.name = name

        # Initialize places
        self.set_places = [Place(f"{name}_SetPlace_{i}") for i in range(N)]
        for place in self.set_places:
            self.add_place(place)

        self.add_item_place = Place(f"{name}_PropertyAddItemPlace")
        self.add_place(self.add_item_place)

        self.remove_item_place = Place(f"{name}_PropertyRemoveItemPlace")
        self.add_place(self.remove_item_place)

        self.set_items_counter_place = Place(f"{name}_PropertySetItemsCounterPlace")
        self.add_place(self.set_items_counter_place)

        self.empty_check_transition = Transition(f"{name}_EventEmptyCheckTransition")
        for place in self.set_places:
            self.empty_check_transition.add_inhibitor_arc(place)
        self.add_transition(self.empty_check_transition)

        # AddToSet transactions
        self.add_to_set_transitions = []
        for i in range(N):
            transition = Transition(f"{name}_AddToSet_{i}")

            for j in range(i+1, N):
                transition.add_inhibitor_arc(self.set_places[j])
            for j in range(0, i):
                transition.From(self.set_places[j])
                transition.To(self.set_places[j])
            transition.To(self.set_places[i])

            self.add_to_set_transitions.append(transition)
            self.add_transition(transition)

        # RemoveFromSet transactions
        self.remove_from_set_transitions = []
        for i in range(N):
            transition = Transition(f"{name}_RemoveFromSet_{i}")
            transition.From(self.set_places[i])

            for j in range(i+1, N):
                transition.add_inhibitor_arc(self.set_places[j])
            for j in range(0, i):
                transition.From(self.set_places[j])
                transition.To(self.set_places[j])

            self.remove_from_set_transitions.append(transition)
            self.add_transition(transition)

        # Connect AddItemPlace to AddToSet transactions
        for transition in self.add_to_set_transitions:
            transition.From(self.add_item_place)
            transition.To(self.set_items_counter_place)

        # Connect RemoveItemPlace to RemoveFromSet transactions
        for transition in self.remove_from_set_transitions:
            transition.From(self.remove_item_place)
            transition.From(self.set_items_counter_place)

class LeaderElection(SubSystem):
    def __init__(self, name, set_system):
        super().__init__(set_system.model)
        self.name = name
        self.set_system = set_system

        # 1) Create a selected place (one)
        self.selected_place = Place(f"{name}_SelectedPlace")
        self.add_place(self.selected_place)

        self.processed_place = Place(f"{name}_ProcessedPlace")
        self.add_place(self.processed_place)

        # 2) For each set_places create a "selection" transaction
        self.selection_transitions = []
        for i, place in enumerate(self.set_system.set_places):
            transition = Transition(f"{name}_SelectionTransition_{i}")

            # Connect to the current place in set_places
            transition.From(place)

            # Connect by inhibitor arc to selected place and processed place
            transition.add_inhibitor_arc(self.selected_place)
            transition.add_inhibitor_arc(self.processed_place)

            # Connect to selected place
            transition.To(self.selected_place)

            self.selection_transitions.append(transition)
            self.add_transition(transition)

        # 3) Create a "processed" place and a "round" transition

        self.round_transition = Transition(f"{name}_RoundTransition")
        self.round_transition.From(self.selected_place)
        self.round_transition.To(self.processed_place)
        self.add_transition(self.round_transition)

        # 4) Create "release" transitions
        self.release_transitions = []
        for i, place in enumerate(self.set_system.set_places):
            transition = Transition(f"{name}_ReleaseTransition_{i}")

            # Connect to "processed"
            transition.From(self.processed_place)

            # Connect to the current place in set_places
            transition.To(place)

            # Add inhibitor arcs to every other place in set_places
            for j, other_place in enumerate(self.set_system.set_places):
                if i != j:
                    transition.add_inhibitor_arc(other_place)

            self.release_transitions.append(transition)
            self.add_transition(transition)

class LeaderVoteLock(SubSystem):
    def __init__(self, name, leader_election):
        super().__init__(leader_election.model)
        self.name = name
        self.leader_election = leader_election

        # 1. Create the two places ActionBeginsPlace and ActionIsRunningPlace
        self.action_begins_place = Place(f"{name}_ActionBeginsPlace")
        self.add_place(self.action_begins_place)

        self.action_is_running_place = Place(f"{name}_ActionIsRunningPlace")
        self.add_place(self.action_is_running_place)

        # 2. Connect to its selected_place with a transaction ActionBeginsTransaction
        self.action_begins_transaction = Transition(f"{name}_ActionBeginsTransaction")
        self.action_begins_transaction.From(self.leader_election.selected_place)
        self.action_begins_transaction.To(self.action_begins_place)
        self.action_begins_transaction.To(self.action_is_running_place)
        self.add_transition(self.action_begins_transaction)

        # 3. Connect LeaderElection round_transition to ActionIsRunningPlace by inhibitor arc
        self.leader_election.round_transition.add_inhibitor_arc(self.action_is_running_place)

        # 4. Create ActionGotDecision place and RoundEnds transition
        self.action_got_decision_place = Place(f"{name}_ActionGotDecisionPlace")
        self.add_place(self.action_got_decision_place)

        self.round_ends_transition = Transition(f"{name}_RoundEndsTransition")
        self.round_ends_transition.From(self.action_got_decision_place)
        self.round_ends_transition.From(self.action_is_running_place)
        self.round_ends_transition.To(self.leader_election.processed_place)
        self.add_transition(self.round_ends_transition)

class VoteOnLeaderAction(SubSystem):
    def __init__(self, name, lock, voters):
        super().__init__(lock.model)
        self.name = name
        self.lock = lock
        self.voters = voters

        # 1. Create the OnFrame transition and connect its From to lock's action_begins_place
        self.on_frame_transition = Transition(f"{name}_OnFrame")
        self.on_frame_transition.From(self.lock.action_begins_place)
        self.add_transition(self.on_frame_transition)

        # 2. For each Voter in voters' set_places, create a place called OnFrameBegins
        # and connect it to the OnFrame transition
        self.on_frame_begins_places = []
        for voter in self.voters.set_places:
            place = Place(f"{name}_OnFrameBegins_{voter.name}")
            self.add_place(place)
            self.on_frame_transition.To(place)
            self.on_frame_begins_places.append(place)

        # 3. For each Voter in voters' set_places, create a place called Active and
        # a transition called NodeActivation
        self.active_places = []
        self.node_activation_transitions = []
        for idx, voter in enumerate(self.voters.set_places):
            active_place = Place(f"{name}_Active_{voter.name}")
            self.add_place(active_place)
            self.active_places.append(active_place)

            node_activation = Transition(f"{name}_NodeActivation_{voter.name}")
            node_activation.From(self.on_frame_begins_places[idx])
            node_activation.From(voter)
            node_activation.To(voter)
            node_activation.To(active_place)
            self.add_transition(node_activation)
            self.node_activation_transitions.append(node_activation)

        # 4. For each Voters' Active place, create ActionAccepted and ActionDeclined places
        # and the transitions ActYes and ActNo
        self.action_accepted_places = []
        self.action_declined_places = []
        self.act_yes_transitions = []
        self.act_no_transitions = []

        for active in self.active_places:
            accepted = Place(f"{name}_ActionAccepted_{active.name}")
            self.add_place(accepted)
            self.action_accepted_places.append(accepted)

            declined = Place(f"{name}_ActionDeclined_{active.name}")
            self.add_place(declined)
            self.action_declined_places.append(declined)

            act_yes = Transition(f"{name}_ActYes_{active.name}")
            act_yes.From(active)
            act_yes.To(accepted)
            self.add_transition(act_yes)
            self.act_yes_transitions.append(act_yes)

            act_no = Transition(f"{name}_ActNo_{active.name}")
            act_no.From(active)
            act_no.To(declined)
            self.add_transition(act_no)
            self.act_no_transitions.append(act_no)

class VotesQuorumCheckerAction(SubSystem):
    def __init__(self, percentage, name, nodes_votes, check_accepted):
        super().__init__(nodes_votes.model)
        self.percentage = percentage
        self.name = name
        self.nodes_votes = nodes_votes

        # 1. Add places: Votes, Quorum, Prune, Pruned, TimeFrameEnd, ConsensusReached, Declined
        self.votes_place = Place(f"{name}_Votes")
        self.add_place(self.votes_place)

        self.quorum_place = Place(f"{name}_Quorum")
        self.add_place(self.quorum_place)

        self.prune_place = Place(f"{name}_Prune")
        self.add_place(self.prune_place)

        self.pruned_place = Place(f"{name}_Pruned")
        self.add_place(self.pruned_place)

        self.consensus_reached_place = Place(f"{name}_ConsensusReached")
        self.add_place(self.consensus_reached_place)

        # 2. For each place P in nodes_votes.action_accepted_places, add transition Gather
        check = []
        if check_accepted:
          check = self.nodes_votes.action_accepted_places
        else:
          check = self.nodes_votes.action_declined_places

        for place in check:
            gather_transition = Transition(f"{name}_Gather_{place.name}")
            gather_transition.From(place)
            gather_transition.To(self.votes_place)
            self.add_transition(gather_transition)

        # 3. Calculate Q and create QuorumChecker transition (all but proposer)
        total_votes = len(check)-1
        Q = int(total_votes * (self.percentage / 100.0))

        quorum_checker_transition = Transition(f"{name}_QuorumChecker")
        quorum_checker_transition.From(self.votes_place, Q)
        quorum_checker_transition.To(self.quorum_place)
        self.add_transition(quorum_checker_transition)

        # 5. Add NotionAccepted transition
        notion_accepted_transition = Transition(f"{name}_NotionAccepted")
        notion_accepted_transition.From(self.quorum_place)
        notion_accepted_transition.To(self.consensus_reached_place)
        self.add_transition(notion_accepted_transition)

        # Adding Prunning
        # 1. initialise:
        notion_accepted_transition.To(self.prune_place)

        # 2. For each gather_transition, add an inhibitor arc checking prune_place is empty
        for transition in self.transitions:
            if "Gather" in transition.name:
                transition.add_inhibitor_arc(self.prune_place)

        # 3. Add a transition that checks via inhibitor arc that Pruned place is empty,
        # takes From votes_place and from Prune place, gives To Prune Place
        prune_transition = Transition(f"{name}_CheckPrune")
        prune_transition.add_inhibitor_arc(self.pruned_place)
        prune_transition.From(self.votes_place)
        prune_transition.From(self.prune_place)
        prune_transition.To(self.prune_place)
        self.add_transition(prune_transition)

        # 4. Add a transition called PrunedQuorum
        # that checks via inhibitor arc that votes_place is empty, takes From Prune and gives To pruned
        pruned_quorum_transition = Transition(f"{name}_PrunedQuorum")
        pruned_quorum_transition.add_inhibitor_arc(self.votes_place)
        pruned_quorum_transition.From(self.prune_place)
        pruned_quorum_transition.To(self.pruned_place)
        self.add_transition(pruned_quorum_transition)

        # 5. Add OnPruned transition that takes From Pruned
        on_pruned_transition = Transition(f"{name}_OnPruned")
        on_pruned_transition.From(self.pruned_place)
        self.add_transition(on_pruned_transition)

class CompositeMutation(SubSystem):
    def __init__(self, model, name, states):
        super().__init__(model)

        self.name = name
        self.states = states

        # Places initialization
        self.place_next = Place(f"{name}_Next")
        self.place_operation_canceled = Place(f"{name}_OperationCanceled")
        self.place_processing = Place(f"{name}_Processing")
        self.place_on_declined = Place(f"{name}_OnDeclined")
        self.place_on_success = Place(f"{name}_OnSuccess")

        self.add_place(self.place_next)
        self.add_place(self.place_operation_canceled)
        self.add_place(self.place_processing)
        self.add_place(self.place_on_declined)
        self.add_place(self.place_on_success)

        # Transitions initialization
        self.transition_got_canceled = Transition(f"{name}_GotCanceled")
        self.transition_got_canceled.From(self.place_operation_canceled)
        self.transition_got_canceled.From(self.place_processing)
        self.transition_got_canceled.To(self.place_on_declined)

        self.transition_got_finished = Transition(f"{name}_GotFinished")
        self.transition_got_finished.From(self.place_processing)
        self.transition_got_finished.To(self.place_on_success)

        self.add_transition(self.transition_got_canceled)
        self.add_transition(self.transition_got_finished)

        # States initialization
        self.places_on_mutation = {}
        self.transitions_got_mutation = {}
        self.transitions_declined = {}

        prev_mutation_place = None
        for state in states:
            place = Place(f"{name}_OnMutation_{state}")
            self.add_place(place)

            self.places_on_mutation[state] = place

            transition_got_mutation = Transition(f"{name}_GotMutation_{state}")
            transition_got_mutation.add_inhibitor_arc(place)
            transition_got_mutation.From(self.place_next)

            if prev_mutation_place:
                transition_got_mutation.From(prev_mutation_place)
            else:
                transition_got_mutation.add_inhibitor_arc(self.place_processing)

            self.add_transition(transition_got_mutation)
            self.transitions_got_mutation[state] = transition_got_mutation

            transition_declined = Transition(f"{name}_Declined_{state}")
            transition_declined.From(place)
            transition_declined.From(self.place_on_declined)

            self.add_transition(transition_declined)
            self.transitions_declined[state] = transition_declined

            prev_mutation_place = place

        # Add the last mutation place to the GotFinished transition
        if prev_mutation_place:
            self.transition_got_finished.From(prev_mutation_place)

class FramedSystem(SubSystem):
    def __init__(self, model, name, operators_set, possible_mutations, mutations_states, consensus_accept_percentage=66.6):
        consensus_decline_percentage = 1 - consensus_accept_percentage
        super().__init__(model)

        self.name = name
        self.model = model
        self.possible_mutations = possible_mutations

        # Create a set of 3 nodes
        self.nodes_set = operators_set
        model.add_subsystem(self.nodes_set)

        # Leader election for the set of nodes
        self.leader_election_system = LeaderElection("LeaderElection", self.nodes_set)
        model.add_subsystem(self.leader_election_system)

        # Add a leader vote lock
        self.leader_vote_lock = LeaderVoteLock("LeaderVoteLock", self.leader_election_system)
        model.add_subsystem(self.leader_vote_lock)

        # Vote on leader action
        self.vote_action = VoteOnLeaderAction("VoteAction", self.leader_vote_lock, self.nodes_set)
        model.add_subsystem(self.vote_action)

        # Add two VotesQuorumCheckerActions

        if consensus_accept_percentage > 0:
          self.vote_checker_accepted = VotesQuorumCheckerAction(consensus_accept_percentage, "AcceptedVoteChecker", self.vote_action, True)
          model.add_subsystem(self.vote_checker_accepted)

        if consensus_decline_percentage > 0:
          self.vote_checker_declined = VotesQuorumCheckerAction(consensus_decline_percentage, "DeclinedVoteChecker", self.vote_action, False)
          model.add_subsystem(self.vote_checker_declined)

        # Expand for PossibleMutations
        self.composite_mutations = {}
        for mutation in self.possible_mutations:
            composite_mutation = CompositeMutation(self.model, mutation, mutations_states[mutation] )
            self.composite_mutations[mutation] = composite_mutation

            if consensus_accept_percentage > 0:
              send_ok_transition = Transition(f"{mutation}_SendOk")
              send_ok_transition.From(self.vote_checker_accepted.consensus_reached_place)
              send_ok_transition.To(composite_mutation.place_next)
              self.add_transition(send_ok_transition)

            if consensus_decline_percentage > 0:
              send_canceled_transition = Transition(f"{mutation}_SendCanceled")
              send_canceled_transition.From(self.vote_checker_declined.consensus_reached_place)
              send_canceled_transition.To(composite_mutation.place_operation_canceled)
              self.add_transition(send_canceled_transition)

# Create the model
model = Model()

# Create a set of three operator nodes
operators_set = ConstSizeSetSubSystem(model, "OperatorsSet", 3)

# List of composite mutations targeting all
composite_mutations_targeting_all = [
    "ChangeOperators",
    "GenerateValidators",
    "AddActiveValidators",
    "StopActiveValidator"
]

# List of composite mutations targeting quorum
composite_mutations_targeting_quorum = [
    "ExitCluster",
    "ExitOperator",
]

# The states for each composite mutation
mutations_states = {
    "GenerateValidators": ["DkgGenerateValidators", "NodeApproveGenerateValidators"],
    "AddActiveValidators": ["ProposeValidatorsStart", "ApproveValidatorsStart", "NodesReady"],
    "StopActiveValidator": ["ProposeValidatorsStop", "ApproveValidatorsStopping"],
    "ChangeOperators": ["ProposeOperators", "ApproveOperators", "OperatorsEnrAck", "ReshareOperatorsState"],
    "ExitCluster": ["DkgAllValidatorsAreFree", "ExitCluster"],
    "ExitOperator": ["ExitOperatorMutation"],
}

# Create the FramedSystem for all voters
framed_system_all = FramedSystem(model, "AllVoters", operators_set, composite_mutations_targeting_all, mutations_states,
                                    consensus_accept_percentage=1)

# Create the FramedSystem for quorum voters with default consensus_accept_percentage
framed_system_quorum = FramedSystem(model, "QuorumVoters", operators_set, composite_mutations_targeting_quorum, mutations_states)

#We assume Cluster is created and basic operators set is configured
exit_operator = framed_system_quorum.composite_mutations["ExitOperator"]
exit_cluster = framed_system_quorum.composite_mutations["ExitCluster"]
change_operators = framed_system_all.composite_mutations["ChangeOperators"]
generate_validators = framed_system_all.composite_mutations["GenerateValidators"]
add_active_validators = framed_system_all.composite_mutations["AddActiveValidators"]
stop_active_validator = framed_system_all.composite_mutations["StopActiveValidator"]

# Using the variables in the function calls
change_operators.transition_got_finished.To(operators_set.add_item_place)
change_operators.transition_got_finished.To(operators_set.remove_item_place)
change_operators.transition_got_finished.To(exit_cluster.place_operation_canceled)
change_operators.transition_got_finished.To(generate_validators.place_operation_canceled)
change_operators.transition_got_finished.To(add_active_validators.place_operation_canceled)
change_operators.transition_got_finished.To(stop_active_validator.place_operation_canceled)
change_operators.transition_got_finished.To(exit_operator.place_operation_canceled)

validators_set = ConstSizeSetSubSystem(model, "ValidatorsSet", 3)
generate_validators.transition_got_finished.To(validators_set.add_item_place)

active_validators_set = ConstSizeSetSubSystem(model, "ActiveValidatorsSet", 3)
stop_active_validator.transition_got_finished.To(validators_set.remove_item_place)

for i, val in enumerate(active_validators_set.set_places):
  can_add_active_validator = Transition(f"CanActivatieValidator_{i}")
  can_add_active_validator.From(add_active_validators.transition_got_finished)
  can_add_active_validator.From(val)
  can_add_active_validator.add_inhibitor_arc(change_operators.place_processing)
  can_add_active_validator.To(val)
  can_add_active_validator.To(active_validators_set.add_item_place)
  model.add_transition(can_add_active_validator)

for place in active_validators_set.set_places:
  exit_cluster.transition_got_finished.add_inhibitor_arc(place)

# Print the network
model.print_network()
```
- Generated model:
  
  pl OperatorsSet_SetPlace_0 (0)
  pl OperatorsSet_SetPlace_1 (0)
  pl OperatorsSet_SetPlace_2 (0)
  pl OperatorsSet_PropertyAddItemPlace (0)
  pl OperatorsSet_PropertyRemoveItemPlace (0)
  pl OperatorsSet_PropertySetItemsCounterPlace (0)
  pl LeaderElection_SelectedPlace (0)
  pl LeaderElection_ProcessedPlace (0)
  pl LeaderVoteLock_ActionBeginsPlace (0)
  pl LeaderVoteLock_ActionIsRunningPlace (0)
  pl LeaderVoteLock_ActionGotDecisionPlace (0)
  pl VoteAction_OnFrameBegins_OperatorsSet_SetPlace_0 (0)
  pl VoteAction_OnFrameBegins_OperatorsSet_SetPlace_1 (0)
  pl VoteAction_OnFrameBegins_OperatorsSet_SetPlace_2 (0)
  pl VoteAction_Active_OperatorsSet_SetPlace_0 (0)
  pl VoteAction_Active_OperatorsSet_SetPlace_1 (0)
  pl VoteAction_Active_OperatorsSet_SetPlace_2 (0)
  pl VoteAction_ActionAccepted_VoteAction_Active_OperatorsSet_SetPlace_0 (0)
  pl VoteAction_ActionDeclined_VoteAction_Active_OperatorsSet_SetPlace_0 (0)
  pl VoteAction_ActionAccepted_VoteAction_Active_OperatorsSet_SetPlace_1 (0)
  pl VoteAction_ActionDeclined_VoteAction_Active_OperatorsSet_SetPlace_1 (0)
  pl VoteAction_ActionAccepted_VoteAction_Active_OperatorsSet_SetPlace_2 (0)
  pl VoteAction_ActionDeclined_VoteAction_Active_OperatorsSet_SetPlace_2 (0)
  pl AcceptedVoteChecker_Votes (0)
  pl AcceptedVoteChecker_Quorum (0)
  pl AcceptedVoteChecker_Prune (0)
  pl AcceptedVoteChecker_Pruned (0)
  pl AcceptedVoteChecker_ConsensusReached (0)
  pl ChangeOperators_Next (0)
  pl ChangeOperators_OperationCanceled (0)
  pl ChangeOperators_Processing (0)
  pl ChangeOperators_OnDeclined (0)
  pl ChangeOperators_OnSuccess (0)
  pl ChangeOperators_OnMutation_ProposeOperators (0)
  pl ChangeOperators_OnMutation_ApproveOperators (0)
  pl ChangeOperators_OnMutation_OperatorsEnrAck (0)
  pl ChangeOperators_OnMutation_ReshareOperatorsState (0)
  pl GenerateValidators_Next (0)
  pl GenerateValidators_OperationCanceled (0)
  pl GenerateValidators_Processing (0)
  pl GenerateValidators_OnDeclined (0)
  pl GenerateValidators_OnSuccess (0)
  pl GenerateValidators_OnMutation_DkgGenerateValidators (0)
  pl GenerateValidators_OnMutation_NodeApproveGenerateValidators (0)
  pl AddActiveValidators_Next (0)
  pl AddActiveValidators_OperationCanceled (0)
  pl AddActiveValidators_Processing (0)
  pl AddActiveValidators_OnDeclined (0)
  pl AddActiveValidators_OnSuccess (0)
  pl AddActiveValidators_OnMutation_ProposeValidatorsStart (0)
  pl AddActiveValidators_OnMutation_ApproveValidatorsStart (0)
  pl AddActiveValidators_OnMutation_NodesReady (0)
  pl StopActiveValidator_Next (0)
  pl StopActiveValidator_OperationCanceled (0)
  pl StopActiveValidator_Processing (0)
  pl StopActiveValidator_OnDeclined (0)
  pl StopActiveValidator_OnSuccess (0)
  pl StopActiveValidator_OnMutation_ProposeValidatorsStop (0)
  pl StopActiveValidator_OnMutation_ApproveValidatorsStopping (0)
  pl LeaderElection_SelectedPlace (0)
  pl LeaderElection_ProcessedPlace (0)
  pl LeaderVoteLock_ActionBeginsPlace (0)
  pl LeaderVoteLock_ActionIsRunningPlace (0)
  pl LeaderVoteLock_ActionGotDecisionPlace (0)
  pl VoteAction_OnFrameBegins_OperatorsSet_SetPlace_0 (0)
  pl VoteAction_OnFrameBegins_OperatorsSet_SetPlace_1 (0)
  pl VoteAction_OnFrameBegins_OperatorsSet_SetPlace_2 (0)
  pl VoteAction_Active_OperatorsSet_SetPlace_0 (0)
  pl VoteAction_Active_OperatorsSet_SetPlace_1 (0)
  pl VoteAction_Active_OperatorsSet_SetPlace_2 (0)
  pl VoteAction_ActionAccepted_VoteAction_Active_OperatorsSet_SetPlace_0 (0)
  pl VoteAction_ActionDeclined_VoteAction_Active_OperatorsSet_SetPlace_0 (0)
  pl VoteAction_ActionAccepted_VoteAction_Active_OperatorsSet_SetPlace_1 (0)
  pl VoteAction_ActionDeclined_VoteAction_Active_OperatorsSet_SetPlace_1 (0)
  pl VoteAction_ActionAccepted_VoteAction_Active_OperatorsSet_SetPlace_2 (0)
  pl VoteAction_ActionDeclined_VoteAction_Active_OperatorsSet_SetPlace_2 (0)
  pl AcceptedVoteChecker_Votes (0)
  pl AcceptedVoteChecker_Quorum (0)
  pl AcceptedVoteChecker_Prune (0)
  pl AcceptedVoteChecker_Pruned (0)
  pl AcceptedVoteChecker_ConsensusReached (0)
  pl ExitCluster_Next (0)
  pl ExitCluster_OperationCanceled (0)
  pl ExitCluster_Processing (0)
  pl ExitCluster_OnDeclined (0)
  pl ExitCluster_OnSuccess (0)
  pl ExitCluster_OnMutation_DkgAllValidatorsAreFree (0)
  pl ExitCluster_OnMutation_ExitCluster (0)
  pl ExitOperator_Next (0)
  pl ExitOperator_OperationCanceled (0)
  pl ExitOperator_Processing (0)
  pl ExitOperator_OnDeclined (0)
  pl ExitOperator_OnSuccess (0)
  pl ExitOperator_OnMutation_ExitOperatorMutation (0)
  pl ValidatorsSet_SetPlace_0 (0)
  pl ValidatorsSet_SetPlace_1 (0)
  pl ValidatorsSet_SetPlace_2 (0)
  pl ValidatorsSet_PropertyAddItemPlace (0)
  pl ValidatorsSet_PropertyRemoveItemPlace (0)
  pl ValidatorsSet_PropertySetItemsCounterPlace (0)
  pl ActiveValidatorsSet_SetPlace_0 (0)
  pl ActiveValidatorsSet_SetPlace_1 (0)
  pl ActiveValidatorsSet_SetPlace_2 (0)
  pl ActiveValidatorsSet_PropertyAddItemPlace (0)
  pl ActiveValidatorsSet_PropertyRemoveItemPlace (0)
  pl ActiveValidatorsSet_PropertySetItemsCounterPlace (0)
  tr {OperatorsSet_EventEmptyCheckTransition} OperatorsSet_SetPlace_0?-1 OperatorsSet_SetPlace_1?-1 OperatorsSet_SetPlace_2?-1 →
  tr {OperatorsSet_AddToSet_0} OperatorsSet_SetPlace_1?-1 OperatorsSet_SetPlace_2?-1 OperatorsSet_PropertyAddItemPlace1 → OperatorsSet_SetPlace_01 OperatorsSet_PropertySetItemsCounterPlace1
  tr {OperatorsSet_AddToSet_1} OperatorsSet_SetPlace_2?-1 OperatorsSet_SetPlace_01 OperatorsSet_PropertyAddItemPlace1 → OperatorsSet_SetPlace_01 OperatorsSet_SetPlace_11 OperatorsSet_PropertySetItemsCounterPlace1
  tr {OperatorsSet_AddToSet_2} OperatorsSet_SetPlace_01 OperatorsSet_SetPlace_11 OperatorsSet_PropertyAddItemPlace1 → OperatorsSet_SetPlace_01 OperatorsSet_SetPlace_11 OperatorsSet_SetPlace_21 OperatorsSet_PropertySetItemsCounterPlace1
  tr {OperatorsSet_RemoveFromSet_0} OperatorsSet_SetPlace_1?-1 OperatorsSet_SetPlace_2?-1 OperatorsSet_SetPlace_01 OperatorsSet_PropertyRemoveItemPlace1 OperatorsSet_PropertySetItemsCounterPlace1 →
  tr {OperatorsSet_RemoveFromSet_1} OperatorsSet_SetPlace_2?-1 OperatorsSet_SetPlace_11 OperatorsSet_SetPlace_01 OperatorsSet_PropertyRemoveItemPlace1 OperatorsSet_PropertySetItemsCounterPlace1 → OperatorsSet_SetPlace_01
  tr {OperatorsSet_RemoveFromSet_2} OperatorsSet_SetPlace_21 OperatorsSet_SetPlace_01 OperatorsSet_SetPlace_11 OperatorsSet_PropertyRemoveItemPlace1 OperatorsSet_PropertySetItemsCounterPlace1 → OperatorsSet_SetPlace_01 OperatorsSet_SetPlace_11
  tr {LeaderElection_SelectionTransition_0} LeaderElection_SelectedPlace?-1 LeaderElection_ProcessedPlace?-1 OperatorsSet_SetPlace_01 → LeaderElection_SelectedPlace1
  tr {LeaderElection_SelectionTransition_1} LeaderElection_SelectedPlace?-1 LeaderElection_ProcessedPlace?-1 OperatorsSet_SetPlace_11 → LeaderElection_SelectedPlace1
  tr {LeaderElection_SelectionTransition_2} LeaderElection_SelectedPlace?-1 LeaderElection_ProcessedPlace?-1 OperatorsSet_SetPlace_21 → LeaderElection_SelectedPlace1
  tr {LeaderElection_RoundTransition} LeaderVoteLock_ActionIsRunningPlace?-1 LeaderElection_SelectedPlace1 → LeaderElection_ProcessedPlace1
  tr {LeaderElection_ReleaseTransition_0} OperatorsSet_SetPlace_1?-1 OperatorsSet_SetPlace_2?-1 LeaderElection_ProcessedPlace1 → OperatorsSet_SetPlace_01
  tr {LeaderElection_ReleaseTransition_1} OperatorsSet_SetPlace_0?-1 OperatorsSet_SetPlace_2?-1 LeaderElection_ProcessedPlace1 → OperatorsSet_SetPlace_11
  tr {LeaderElection_ReleaseTransition_2} OperatorsSet_SetPlace_0?-1 OperatorsSet_SetPlace_1?-1 LeaderElection_ProcessedPlace1 → OperatorsSet_SetPlace_21
  tr {LeaderVoteLock_ActionBeginsTransaction} LeaderElection_SelectedPlace1 → LeaderVoteLock_ActionBeginsPlace1 LeaderVoteLock_ActionIsRunningPlace1
  tr {LeaderVoteLock_RoundEndsTransition} LeaderVoteLock_ActionGotDecisionPlace1 LeaderVoteLock_ActionIsRunningPlace1 → LeaderElection_ProcessedPlace1
  tr {VoteAction_OnFrame} LeaderVoteLock_ActionBeginsPlace1 → VoteAction_OnFrameBegins_OperatorsSet_SetPlace_01 VoteAction_OnFrameBegins_OperatorsSet_SetPlace_11 VoteAction_OnFrameBegins_OperatorsSet_SetPlace_21
  tr {VoteAction_NodeActivation_OperatorsSet_SetPlace_0} VoteAction_OnFrameBegins_OperatorsSet_SetPlace_01 OperatorsSet_SetPlace_01 → OperatorsSet_SetPlace_01 VoteAction_Active_OperatorsSet_SetPlace_01
  tr {VoteAction_NodeActivation_OperatorsSet_SetPlace_1} VoteAction_OnFrameBegins_OperatorsSet_SetPlace_11 OperatorsSet_SetPlace_11 → OperatorsSet_SetPlace_11 VoteAction_Active_OperatorsSet_SetPlace_11
  tr {VoteAction_NodeActivation_OperatorsSet_SetPlace_2} VoteAction_OnFrameBegins_OperatorsSet_SetPlace_21 OperatorsSet_SetPlace_21 → OperatorsSet_SetPlace_21 VoteAction_Active_OperatorsSet_SetPlace_21
  tr {VoteAction_ActYes_VoteAction_Active_OperatorsSet_SetPlace_0} VoteAction_Active_OperatorsSet_SetPlace_01 → VoteAction_ActionAccepted_VoteAction_Active_OperatorsSet_SetPlace_01
  tr {VoteAction_ActNo_VoteAction_Active_OperatorsSet_SetPlace_0} VoteAction_Active_OperatorsSet_SetPlace_01 → VoteAction_ActionDeclined_VoteAction_Active_OperatorsSet_SetPlace_01
  tr {VoteAction_ActYes_VoteAction_Active_OperatorsSet_SetPlace_1} VoteAction_Active_OperatorsSet_SetPlace_11 → VoteAction_ActionAccepted_VoteAction_Active_OperatorsSet_SetPlace_11
  tr {VoteAction_ActNo_VoteAction_Active_OperatorsSet_SetPlace_1} VoteAction_Active_OperatorsSet_SetPlace_11 → VoteAction_ActionDeclined_VoteAction_Active_OperatorsSet_SetPlace_11
  tr {VoteAction_ActYes_VoteAction_Active_OperatorsSet_SetPlace_2} VoteAction_Active_OperatorsSet_SetPlace_21 → VoteAction_ActionAccepted_VoteAction_Active_OperatorsSet_SetPlace_21
  tr {VoteAction_ActNo_VoteAction_Active_OperatorsSet_SetPlace_2} VoteAction_Active_OperatorsSet_SetPlace_21 → VoteAction_ActionDeclined_VoteAction_Active_OperatorsSet_SetPlace_21
  tr {AcceptedVoteChecker_Gather_VoteAction_ActionAccepted_VoteAction_Active_OperatorsSet_SetPlace_0} AcceptedVoteChecker_Prune?-1 VoteAction_ActionAccepted_VoteAction_Active_OperatorsSet_SetPlace_01 → AcceptedVoteChecker_Votes1
  tr {AcceptedVoteChecker_Gather_VoteAction_ActionAccepted_VoteAction_Active_OperatorsSet_SetPlace_1} AcceptedVoteChecker_Prune?-1 VoteAction_ActionAccepted_VoteAction_Active_OperatorsSet_SetPlace_11 → AcceptedVoteChecker_Votes1
  tr {AcceptedVoteChecker_Gather_VoteAction_ActionAccepted_VoteAction_Active_OperatorsSet_SetPlace_2} AcceptedVoteChecker_Prune?-1 VoteAction_ActionAccepted_VoteAction_Active_OperatorsSet_SetPlace_21 → AcceptedVoteChecker_Votes1
  tr {AcceptedVoteChecker_QuorumChecker} AcceptedVoteChecker_Votes0 → AcceptedVoteChecker_Quorum1
  tr {AcceptedVoteChecker_NotionAccepted} AcceptedVoteChecker_Quorum1 → AcceptedVoteChecker_ConsensusReached1 AcceptedVoteChecker_Prune1
  tr {AcceptedVoteChecker_CheckPrune} AcceptedVoteChecker_Pruned?-1 AcceptedVoteChecker_Votes1 AcceptedVoteChecker_Prune1 → AcceptedVoteChecker_Prune1
  tr {AcceptedVoteChecker_PrunedQuorum} AcceptedVoteChecker_Votes?-1 AcceptedVoteChecker_Prune1 → AcceptedVoteChecker_Pruned1
  tr {AcceptedVoteChecker_OnPruned} AcceptedVoteChecker_Pruned1 →
  tr {ChangeOperators_GotCanceled} ChangeOperators_OperationCanceled1 ChangeOperators_Processing1 → ChangeOperators_OnDeclined1
  tr {ChangeOperators_GotFinished} ChangeOperators_Processing1 ChangeOperators_OnMutation_ReshareOperatorsState1 → ChangeOperators_OnSuccess1 OperatorsSet_PropertyAddItemPlace1 OperatorsSet_PropertyRemoveItemPlace1 ExitCluster_OperationCanceled1 GenerateValidators_OperationCanceled1 AddActiveValidators_OperationCanceled1 StopActiveValidator_OperationCanceled1 ExitOperator_OperationCanceled1
  tr {ChangeOperators_GotMutation_ProposeOperators} ChangeOperators_OnMutation_ProposeOperators?-1 ChangeOperators_Processing?-1 ChangeOperators_Next1 →
  tr {ChangeOperators_Declined_ProposeOperators} ChangeOperators_OnMutation_ProposeOperators1 ChangeOperators_OnDeclined1 →
  tr {ChangeOperators_GotMutation_ApproveOperators} ChangeOperators_OnMutation_ApproveOperators?-1 ChangeOperators_Next1 ChangeOperators_OnMutation_ProposeOperators1 →
  tr {ChangeOperators_Declined_ApproveOperators} ChangeOperators_OnMutation_ApproveOperators1 ChangeOperators_OnDeclined1 →
  tr {ChangeOperators_GotMutation_OperatorsEnrAck} ChangeOperators_OnMutation_OperatorsEnrAck?-1 ChangeOperators_Next1 ChangeOperators_OnMutation_ApproveOperators1 →
  tr {ChangeOperators_Declined_OperatorsEnrAck} ChangeOperators_OnMutation_OperatorsEnrAck1 ChangeOperators_OnDeclined1 →
  tr {ChangeOperators_GotMutation_ReshareOperatorsState} ChangeOperators_OnMutation_ReshareOperatorsState?-1 ChangeOperators_Next1 ChangeOperators_OnMutation_OperatorsEnrAck1 →
  tr {ChangeOperators_Declined_ReshareOperatorsState} ChangeOperators_OnMutation_ReshareOperatorsState1 ChangeOperators_OnDeclined1 →
  tr {ChangeOperators_SendOk} AcceptedVoteChecker_ConsensusReached1 → ChangeOperators_Next1
  tr {GenerateValidators_GotCanceled} GenerateValidators_OperationCanceled1 GenerateValidators_Processing1 → GenerateValidators_OnDeclined1
  tr {GenerateValidators_GotFinished} GenerateValidators_Processing1 GenerateValidators_OnMutation_NodeApproveGenerateValidators1 → GenerateValidators_OnSuccess1 ValidatorsSet_PropertyAddItemPlace1
  tr {GenerateValidators_GotMutation_DkgGenerateValidators} GenerateValidators_OnMutation_DkgGenerateValidators?-1 GenerateValidators_Processing?-1 GenerateValidators_Next1 →
  tr {GenerateValidators_Declined_DkgGenerateValidators} GenerateValidators_OnMutation_DkgGenerateValidators1 GenerateValidators_OnDeclined1 →
  tr {GenerateValidators_GotMutation_NodeApproveGenerateValidators} GenerateValidators_OnMutation_NodeApproveGenerateValidators?-1 GenerateValidators_Next1 GenerateValidators_OnMutation_DkgGenerateValidators1 →
  tr {GenerateValidators_Declined_NodeApproveGenerateValidators} GenerateValidators_OnMutation_NodeApproveGenerateValidators1 GenerateValidators_OnDeclined1 →
  tr {GenerateValidators_SendOk} AcceptedVoteChecker_ConsensusReached1 → GenerateValidators_Next1
  tr {AddActiveValidators_GotCanceled} AddActiveValidators_OperationCanceled1 AddActiveValidators_Processing1 → AddActiveValidators_OnDeclined1
  tr {AddActiveValidators_GotFinished} AddActiveValidators_Processing1 AddActiveValidators_OnMutation_NodesReady1 → AddActiveValidators_OnSuccess1
  tr {AddActiveValidators_GotMutation_ProposeValidatorsStart} AddActiveValidators_OnMutation_ProposeValidatorsStart?-1 AddActiveValidators_Processing?-1 AddActiveValidators_Next1 →
  tr {AddActiveValidators_Declined_ProposeValidatorsStart} AddActiveValidators_OnMutation_ProposeValidatorsStart1 AddActiveValidators_OnDeclined1 →
  tr {AddActiveValidators_GotMutation_ApproveValidatorsStart} AddActiveValidators_OnMutation_ApproveValidatorsStart?-1 AddActiveValidators_Next1 AddActiveValidators_OnMutation_ProposeValidatorsStart1 →
  tr {AddActiveValidators_Declined_ApproveValidatorsStart} AddActiveValidators_OnMutation_ApproveValidatorsStart1 AddActiveValidators_OnDeclined1 →
  tr {AddActiveValidators_GotMutation_NodesReady} AddActiveValidators_OnMutation_NodesReady?-1 AddActiveValidators_Next1 AddActiveValidators_OnMutation_ApproveValidatorsStart1 →
  tr {AddActiveValidators_Declined_NodesReady} AddActiveValidators_OnMutation_NodesReady1 AddActiveValidators_OnDeclined1 →
  tr {AddActiveValidators_SendOk} AcceptedVoteChecker_ConsensusReached1 → AddActiveValidators_Next1
  tr {StopActiveValidator_GotCanceled} StopActiveValidator_OperationCanceled1 StopActiveValidator_Processing1 → StopActiveValidator_OnDeclined1
  tr {StopActiveValidator_GotFinished} StopActiveValidator_Processing1 StopActiveValidator_OnMutation_ApproveValidatorsStopping1 → StopActiveValidator_OnSuccess1 ValidatorsSet_PropertyRemoveItemPlace1
  tr {StopActiveValidator_GotMutation_ProposeValidatorsStop} StopActiveValidator_OnMutation_ProposeValidatorsStop?-1 StopActiveValidator_Processing?-1 StopActiveValidator_Next1 →
  tr {StopActiveValidator_Declined_ProposeValidatorsStop} StopActiveValidator_OnMutation_ProposeValidatorsStop1 StopActiveValidator_OnDeclined1 →
  tr {StopActiveValidator_GotMutation_ApproveValidatorsStopping} StopActiveValidator_OnMutation_ApproveValidatorsStopping?-1 StopActiveValidator_Next1 StopActiveValidator_OnMutation_ProposeValidatorsStop1 →
  tr {StopActiveValidator_Declined_ApproveValidatorsStopping} StopActiveValidator_OnMutation_ApproveValidatorsStopping1 StopActiveValidator_OnDeclined1 →
  tr {StopActiveValidator_SendOk} AcceptedVoteChecker_ConsensusReached1 → StopActiveValidator_Next1
  tr {LeaderElection_SelectionTransition_0} LeaderElection_SelectedPlace?-1 LeaderElection_ProcessedPlace?-1 OperatorsSet_SetPlace_01 → LeaderElection_SelectedPlace1
  tr {LeaderElection_SelectionTransition_1} LeaderElection_SelectedPlace?-1 LeaderElection_ProcessedPlace?-1 OperatorsSet_SetPlace_11 → LeaderElection_SelectedPlace1
  tr {LeaderElection_SelectionTransition_2} LeaderElection_SelectedPlace?-1 LeaderElection_ProcessedPlace?-1 OperatorsSet_SetPlace_21 → LeaderElection_SelectedPlace1
  tr {LeaderElection_RoundTransition} LeaderVoteLock_ActionIsRunningPlace?-1 LeaderElection_SelectedPlace1 → LeaderElection_ProcessedPlace1
  tr {LeaderElection_ReleaseTransition_0} OperatorsSet_SetPlace_1?-1 OperatorsSet_SetPlace_2?-1 LeaderElection_ProcessedPlace1 → OperatorsSet_SetPlace_01
  tr {LeaderElection_ReleaseTransition_1} OperatorsSet_SetPlace_0?-1 OperatorsSet_SetPlace_2?-1 LeaderElection_ProcessedPlace1 → OperatorsSet_SetPlace_11
  tr {LeaderElection_ReleaseTransition_2} OperatorsSet_SetPlace_0?-1 OperatorsSet_SetPlace_1?-1 LeaderElection_ProcessedPlace1 → OperatorsSet_SetPlace_21
  tr {LeaderVoteLock_ActionBeginsTransaction} LeaderElection_SelectedPlace1 → LeaderVoteLock_ActionBeginsPlace1 LeaderVoteLock_ActionIsRunningPlace1
  tr {LeaderVoteLock_RoundEndsTransition} LeaderVoteLock_ActionGotDecisionPlace1 LeaderVoteLock_ActionIsRunningPlace1 → LeaderElection_ProcessedPlace1
  tr {VoteAction_OnFrame} LeaderVoteLock_ActionBeginsPlace1 → VoteAction_OnFrameBegins_OperatorsSet_SetPlace_01 VoteAction_OnFrameBegins_OperatorsSet_SetPlace_11 VoteAction_OnFrameBegins_OperatorsSet_SetPlace_21
  tr {VoteAction_NodeActivation_OperatorsSet_SetPlace_0} VoteAction_OnFrameBegins_OperatorsSet_SetPlace_01 OperatorsSet_SetPlace_01 → OperatorsSet_SetPlace_01 VoteAction_Active_OperatorsSet_SetPlace_01
  tr {VoteAction_NodeActivation_OperatorsSet_SetPlace_1} VoteAction_OnFrameBegins_OperatorsSet_SetPlace_11 OperatorsSet_SetPlace_11 → OperatorsSet_SetPlace_11 VoteAction_Active_OperatorsSet_SetPlace_11
  tr {VoteAction_NodeActivation_OperatorsSet_SetPlace_2} VoteAction_OnFrameBegins_OperatorsSet_SetPlace_21 OperatorsSet_SetPlace_21 → OperatorsSet_SetPlace_21 VoteAction_Active_OperatorsSet_SetPlace_21
  tr {VoteAction_ActYes_VoteAction_Active_OperatorsSet_SetPlace_0} VoteAction_Active_OperatorsSet_SetPlace_01 → VoteAction_ActionAccepted_VoteAction_Active_OperatorsSet_SetPlace_01
  tr {VoteAction_ActNo_VoteAction_Active_OperatorsSet_SetPlace_0} VoteAction_Active_OperatorsSet_SetPlace_01 → VoteAction_ActionDeclined_VoteAction_Active_OperatorsSet_SetPlace_01
  tr {VoteAction_ActYes_VoteAction_Active_OperatorsSet_SetPlace_1} VoteAction_Active_OperatorsSet_SetPlace_11 → VoteAction_ActionAccepted_VoteAction_Active_OperatorsSet_SetPlace_11
  tr {VoteAction_ActNo_VoteAction_Active_OperatorsSet_SetPlace_1} VoteAction_Active_OperatorsSet_SetPlace_11 → VoteAction_ActionDeclined_VoteAction_Active_OperatorsSet_SetPlace_11
  tr {VoteAction_ActYes_VoteAction_Active_OperatorsSet_SetPlace_2} VoteAction_Active_OperatorsSet_SetPlace_21 → VoteAction_ActionAccepted_VoteAction_Active_OperatorsSet_SetPlace_21
  tr {VoteAction_ActNo_VoteAction_Active_OperatorsSet_SetPlace_2} VoteAction_Active_OperatorsSet_SetPlace_21 → VoteAction_ActionDeclined_VoteAction_Active_OperatorsSet_SetPlace_21
  tr {AcceptedVoteChecker_Gather_VoteAction_ActionAccepted_VoteAction_Active_OperatorsSet_SetPlace_0} AcceptedVoteChecker_Prune?-1 VoteAction_ActionAccepted_VoteAction_Active_OperatorsSet_SetPlace_01 → AcceptedVoteChecker_Votes1
  tr {AcceptedVoteChecker_Gather_VoteAction_ActionAccepted_VoteAction_Active_OperatorsSet_SetPlace_1} AcceptedVoteChecker_Prune?-1 VoteAction_ActionAccepted_VoteAction_Active_OperatorsSet_SetPlace_11 → AcceptedVoteChecker_Votes1
  tr {AcceptedVoteChecker_Gather_VoteAction_ActionAccepted_VoteAction_Active_OperatorsSet_SetPlace_2} AcceptedVoteChecker_Prune?-1 VoteAction_ActionAccepted_VoteAction_Active_OperatorsSet_SetPlace_21 → AcceptedVoteChecker_Votes1
  tr {AcceptedVoteChecker_QuorumChecker} AcceptedVoteChecker_Votes1 → AcceptedVoteChecker_Quorum1
  tr {AcceptedVoteChecker_NotionAccepted} AcceptedVoteChecker_Quorum1 → AcceptedVoteChecker_ConsensusReached1 AcceptedVoteChecker_Prune1
  tr {AcceptedVoteChecker_CheckPrune} AcceptedVoteChecker_Pruned?-1 AcceptedVoteChecker_Votes1 AcceptedVoteChecker_Prune1 → AcceptedVoteChecker_Prune1
  tr {AcceptedVoteChecker_PrunedQuorum} AcceptedVoteChecker_Votes?-1 AcceptedVoteChecker_Prune1 → AcceptedVoteChecker_Pruned1
  tr {AcceptedVoteChecker_OnPruned} AcceptedVoteChecker_Pruned1 →
  tr {ExitCluster_GotCanceled} ExitCluster_OperationCanceled1 ExitCluster_Processing1 → ExitCluster_OnDeclined1
  tr {ExitCluster_GotFinished} ActiveValidatorsSet_SetPlace_0?-1 ActiveValidatorsSet_SetPlace_1?-1 ActiveValidatorsSet_SetPlace_2?-1 ExitCluster_Processing1 ExitCluster_OnMutation_ExitCluster1 → ExitCluster_OnSuccess1
  tr {ExitCluster_GotMutation_DkgAllValidatorsAreFree} ExitCluster_OnMutation_DkgAllValidatorsAreFree?-1 ExitCluster_Processing?-1 ExitCluster_Next1 →
  tr {ExitCluster_Declined_DkgAllValidatorsAreFree} ExitCluster_OnMutation_DkgAllValidatorsAreFree1 ExitCluster_OnDeclined1 →
  tr {ExitCluster_GotMutation_ExitCluster} ExitCluster_OnMutation_ExitCluster?-1 ExitCluster_Next1 ExitCluster_OnMutation_DkgAllValidatorsAreFree1 →
  tr {ExitCluster_Declined_ExitCluster} ExitCluster_OnMutation_ExitCluster1 ExitCluster_OnDeclined1 →
  tr {ExitCluster_SendOk} AcceptedVoteChecker_ConsensusReached1 → ExitCluster_Next1
  tr {ExitOperator_GotCanceled} ExitOperator_OperationCanceled1 ExitOperator_Processing1 → ExitOperator_OnDeclined1
  tr {ExitOperator_GotFinished} ExitOperator_Processing1 ExitOperator_OnMutation_ExitOperatorMutation1 → ExitOperator_OnSuccess1
  tr {ExitOperator_GotMutation_ExitOperatorMutation} ExitOperator_OnMutation_ExitOperatorMutation?-1 ExitOperator_Processing?-1 ExitOperator_Next1 →
  tr {ExitOperator_Declined_ExitOperatorMutation} ExitOperator_OnMutation_ExitOperatorMutation1 ExitOperator_OnDeclined1 →
  tr {ExitOperator_SendOk} AcceptedVoteChecker_ConsensusReached1 → ExitOperator_Next1
  tr {ValidatorsSet_EventEmptyCheckTransition} ValidatorsSet_SetPlace_0?-1 ValidatorsSet_SetPlace_1?-1 ValidatorsSet_SetPlace_2?-1 →
  tr {ValidatorsSet_AddToSet_0} ValidatorsSet_SetPlace_1?-1 ValidatorsSet_SetPlace_2?-1 ValidatorsSet_PropertyAddItemPlace1 → ValidatorsSet_SetPlace_01 ValidatorsSet_PropertySetItemsCounterPlace1
  tr {ValidatorsSet_AddToSet_1} ValidatorsSet_SetPlace_2?-1 ValidatorsSet_SetPlace_01 ValidatorsSet_PropertyAddItemPlace1 → ValidatorsSet_SetPlace_01 ValidatorsSet_SetPlace_11 ValidatorsSet_PropertySetItemsCounterPlace1
  tr {ValidatorsSet_AddToSet_2} ValidatorsSet_SetPlace_01 ValidatorsSet_SetPlace_11 ValidatorsSet_PropertyAddItemPlace1 → ValidatorsSet_SetPlace_01 ValidatorsSet_SetPlace_11 ValidatorsSet_SetPlace_21 ValidatorsSet_PropertySetItemsCounterPlace1
  tr {ValidatorsSet_RemoveFromSet_0} ValidatorsSet_SetPlace_1?-1 ValidatorsSet_SetPlace_2?-1 ValidatorsSet_SetPlace_01 ValidatorsSet_PropertyRemoveItemPlace1 ValidatorsSet_PropertySetItemsCounterPlace1 →
  tr {ValidatorsSet_RemoveFromSet_1} ValidatorsSet_SetPlace_2?-1 ValidatorsSet_SetPlace_11 ValidatorsSet_SetPlace_01 ValidatorsSet_PropertyRemoveItemPlace1 ValidatorsSet_PropertySetItemsCounterPlace1 → ValidatorsSet_SetPlace_01
  tr {ValidatorsSet_RemoveFromSet_2} ValidatorsSet_SetPlace_21 ValidatorsSet_SetPlace_01 ValidatorsSet_SetPlace_11 ValidatorsSet_PropertyRemoveItemPlace1 ValidatorsSet_PropertySetItemsCounterPlace1 → ValidatorsSet_SetPlace_01 ValidatorsSet_SetPlace_11
  tr {ActiveValidatorsSet_EventEmptyCheckTransition} ActiveValidatorsSet_SetPlace_0?-1 ActiveValidatorsSet_SetPlace_1?-1 ActiveValidatorsSet_SetPlace_2?-1 →
  tr {ActiveValidatorsSet_AddToSet_0} ActiveValidatorsSet_SetPlace_1?-1 ActiveValidatorsSet_SetPlace_2?-1 ActiveValidatorsSet_PropertyAddItemPlace1 → ActiveValidatorsSet_SetPlace_01 ActiveValidatorsSet_PropertySetItemsCounterPlace1
  tr {ActiveValidatorsSet_AddToSet_1} ActiveValidatorsSet_SetPlace_2?-1 ActiveValidatorsSet_SetPlace_01 ActiveValidatorsSet_PropertyAddItemPlace1 → ActiveValidatorsSet_SetPlace_01 ActiveValidatorsSet_SetPlace_11 ActiveValidatorsSet_PropertySetItemsCounterPlace1
  tr {ActiveValidatorsSet_AddToSet_2} ActiveValidatorsSet_SetPlace_01 ActiveValidatorsSet_SetPlace_11 ActiveValidatorsSet_PropertyAddItemPlace1 → ActiveValidatorsSet_SetPlace_01 ActiveValidatorsSet_SetPlace_11 ActiveValidatorsSet_SetPlace_21 ActiveValidatorsSet_PropertySetItemsCounterPlace1
  tr {ActiveValidatorsSet_RemoveFromSet_0} ActiveValidatorsSet_SetPlace_1?-1 ActiveValidatorsSet_SetPlace_2?-1 ActiveValidatorsSet_SetPlace_01 ActiveValidatorsSet_PropertyRemoveItemPlace1 ActiveValidatorsSet_PropertySetItemsCounterPlace1 →
  tr {ActiveValidatorsSet_RemoveFromSet_1} ActiveValidatorsSet_SetPlace_2?-1 ActiveValidatorsSet_SetPlace_11 ActiveValidatorsSet_SetPlace_01 ActiveValidatorsSet_PropertyRemoveItemPlace1 ActiveValidatorsSet_PropertySetItemsCounterPlace1 → ActiveValidatorsSet_SetPlace_01
  tr {ActiveValidatorsSet_RemoveFromSet_2} ActiveValidatorsSet_SetPlace_21 ActiveValidatorsSet_SetPlace_01 ActiveValidatorsSet_SetPlace_11 ActiveValidatorsSet_PropertyRemoveItemPlace1 ActiveValidatorsSet_PropertySetItemsCounterPlace1 → ActiveValidatorsSet_SetPlace_01 ActiveValidatorsSet_SetPlace_11
  tr {CanActivatieValidator_0} ChangeOperators_Processing?-1 AddActiveValidators_GotFinished1 ActiveValidatorsSet_SetPlace_01 → ActiveValidatorsSet_SetPlace_01 ActiveValidatorsSet_PropertyAddItemPlace1
  tr {CanActivatieValidator_1} ChangeOperators_Processing?-1 AddActiveValidators_GotFinished1 ActiveValidatorsSet_SetPlace_11 → ActiveValidatorsSet_SetPlace_11 ActiveValidatorsSet_PropertyAddItemPlace1
  tr {CanActivatieValidator_2} ChangeOperators_Processing?-1 AddActiveValidators_GotFinished1 ActiveValidatorsSet_SetPlace_21 → ActiveValidatorsSet_SetPlace_21 ActiveValidatorsSet_PropertyAddItemPlace*1
  net buffer
Generated example visualised as raw PN format (large digraph):

Generated network and its incividual components can be formally modeled and verified in Petri Nets modelling tool such as [SMPT](https://github.com/nicolasAmat/SMPT/tree/master) and [Nd](https://projects.laas.fr/tina/download.php) that support .net format with inhibitor nodes by setting various default states for operations, operators and validators (putting markers into places) and testing desired configuration of a given network.

Given that BFT protocol implementation algorithm is out of scope and we can construct Blockchain or DAG using given base state consensus synchronizing solution, also not all of the state change decisions of operators can be automated as some synchronisation happens in the background in off-chain

Topic		Replies	Views
Proposal: Attributable Consensus Solution for DV Clusters -- Part 2 💡 Obol Protocol	0	345	December 19, 2023
Proposal: Attributable Consensus Solution for DV Clusters 💡 Obol Protocol	2	568	January 15, 2024
Proposal: Attributable Consensus Solution for DV Clusters – Part 3 💡 Obol Protocol	0	273	January 4, 2024
Proposal: Key Refresh Scheme for DV operators 💡 Obol Protocol	0	596	November 22, 2023
Proposal: Using DV clusters for encrypted transaction mempools 💡 Obol Protocol	0	673	December 29, 2023