Crate taco_acs_model_checker 

Abstract Counter System Model Checker

This crate implements a counter system based model checker as described in the paper “Parameterized Verification of Round-based Distributed Algorithms via Extended Threshold Automata”. This model checker will construct the explicit counter system (ACS in the paper), starting from potential error states and checking whether an initial state is reachable. If a path is found, the SMT checker will be used to check whether the path is spurious.

Note that this model checker does not support “reachability” specifications, i.e. specifications, that require a location to be not covered by any process.

Modules

acs_threshold_automaton

A ThresholdAutomaton representation for efficient operations on counter systems and counter configurations

error_graph

Error Graph

partial_ord

Custom Partial Order Trait

Structs

ACSModelChecker

Counter system based model checker

Enums

ACSModelCheckerInitializationError