PyNuSMV is distributed with some tools developed thanks to the library. These tools serve as examples of how to use PyNuSMV and what can be achieved. This section describes the tools currently distributed with PyNuSMV.


Tree-Like Annotated Counter-Examples
--------------------------------------------------------------------------------

This tool is provided in the tools.tlace package.
     
Tree-Like Annotated Counter-Examples (TLACEs for short) are rich branching counter-examples [BP12]. This tool extends NuSMV explanations to produce these rich counter-examples instead of single paths. It uses NuSMV model checking algorithms and path explanation generators (ex_explain, eg_explain, eu_explain), the parser for CTL formulas, etc. The result is a tool taking an SMV model as argument, checking all CTL properties of the model and producing TLACEs when the property is violated.

To run this tool, launch the following command from the src/ directory of PyNuSMV package.

python -m tools.tlace.tlace MODEL

where MODEL is an SMV model. The tool computes the given model, check all its CTL specifications and produces a TLACE explaining why each violated specification is violated.

    
ARCTL with TLACE generation
--------------------------------------------------------------------------------
     
Action-Restricted CTL (ARCTL for short) is an extension of CTL where quantified paths are restricted to paths of actions satisfying a propositional property [PR07]. This tool is defined in the tools.arctl package.

It performs ARCTL model checking on SMV models and produces counter-examples and witnesses to explain ARCTL properties violation or satisfaction. These diagnostics can be either simple paths of the system or full TLACEs; TLACEs are defined in the separated sub-package tools.arctl.tlace.

Finally, this tool provides two CLI to use these functionalities; these CLI are defined in the sub-package tools.arctl.cmd. tools.arctl.cmd.trace is a CLI that allows to read a system from an SMV model and to check ARCTL specifications over it. Whatever the result of the verification, this CLI produces a diagnostic to explain the verification outcome. This CLI produces simple paths of the system as diagnostics. On the other hand, tools.arctl.cmd.tlace provides the same functionalities but produces TLACEs as diagnostics.

To run this tool, launch the following command from the src/ directory of PyNuSMV package.

python -m tools.arctl.cmd.trace

This gives a prompt accepting some commands. The list of accepted commands can be shown using the help command.

To launch the CLI producing TLACEs. Just run the same command with tlace instead of trace; accepted commands are the same.
	
	
CTLK model checking and TLACE generation and exploration
--------------------------------------------------------------------------------

CTLK is an extension of CTLK allowing to reason about time and knowledge of the agents of a system [PL03]. This logic is interpreted over systems composed of agents that have a limited knowledge of the system current state. It allows to mix temporal and epistemic operators to express, for example, that at all time, an agent knows that a property is true.

This tool performs model checking of CTLK on multi-agent systems defined with the SMV language. Il also generates diagnostics for explaining verification outcomes. Finally, it allows the user to interactively explore a TLACE explaining the result of verification.

More precisely, this tool accepts any SMV model and follows these conventions:
    - any instance of a module declared in the "main" module is considered an agent;
    - the direct knowledge of an agent is given by all its local variables, i.e. the variables declared in its module, and by all its arguments that are variables.

To run this tool, launch the following command from the src/ directory of PyNuSMV package.

python -m tools.ctlk.cmd.cmd

This gives a prompt accepting some commands listed by the "help" command. This prompt accepts, for example, the "model" command to specify an SMV model, the "check" command to verify a CTLK property, or the "explain" command to explain the model checking result. In particular, the "explain" command opens another prompt to explore the diagnostic; the help can be accessed through the "help" command. Finally, note that any command has its own help message, accessible through the "help <cmd>" command.


CTL model checking
--------------------------------------------------------------------------------

PyNuSMV is shipped with a reimplementation of CTL model checking, for performance measures. This tool can be run with

python -m tools.ctl.CTLcheck [model]

where [model] is the path to a NuSMV model. The tool loads the model, checks every CTL specification in the model file and outputs its truth value.


Fair CTL model checking
--------------------------------------------------------------------------------

A reimplementation of Fair CTL model checking is provided. This tool can be run with

python -m tools.fairctl.FairCTLcheck [model]

where model is the path to a NuSMV model. The tool loads the model, checks every CTL specification in the model file (under fairness constraints of the model) and outputs its truth value.


Multi-agent systems
--------------------------------------------------------------------------------

An implementation of Multi-agent systems (MAS) is provided with PyNuSMV. The tool is a library to define and manipulate MASs with NuSMV. To load a model and get the corresponding MAS, you have to use tools.mas.glob to load a model (load_from_file function) and to get the MAS (mas function).

On a MAS, you can perform any action given by a PyNuSMV BddFsm, plus additional functionalities like getting equivalent states according to a set of agents' knowledge or getting the protocol of any subset of agents (see tools.mas.mas for more information).

The assumptions on the given SMV model representing a MAS are the following:
 - Every module instance of the MAIN module is considered as an agent;
 - The agent's name is the variable name of the instance;
 - The knowledge of the agent (its observations) are its internal state variables (the variables beginning with agent's name) and all variables given as a parameter at instanciation of the module (only pure variables are considered, not expressions or input variables).


ATL model checking
--------------------------------------------------------------------------------

An implementation of ATL model checking is provided, relying on the MAS library. This tool can be run with

python -m tools.atl.check [model]

where model is the path to an SMV model representing a Multi-agent system (see above). The tool loads the model and starts a minimal command-line interface. Every typed ATL formula is checked and the result of the verification is given at standard output. The command-line interface can be exited with EOF (CTRL-D).

The grammar for ATL properties phi is the following:

phi ::= EXPR | '(' phi ')' | phi '&' phi | phi '|' phi | '~'phi | phi '->' phi
        | phi '<->' phi | '<' group '>' psi | '[' GROUP ']' psi
psi ::= 'X' phi | 'G' phi | 'F' phi | '[' phi 'U' phi ']' | '[' phi 'W' phi ']'

where EXPR is any simple expression over variables of the system, enclosed into simple quotes (e.g. EXPR = 'transmission = completed' or EXPR = 'v = 3'), and GROUP is a list of agent names enclosed into simple quotes, separated by commas (e.g. GROUP = 'sender', 'transmitter' or GROUP = 'dealer').


Model checking ATLK with full and partial observability
--------------------------------------------------------------------------------

An implementation of model checking algorithms for ATLK with full and partial observability [BPQR13] is provided. This tool can be run with

python -m tools.atlkFO.check [model]

for the full observability setting, and with

python -m tools.atlkPO.check [model]

for the partial observability setting.

[model] is the path to an SMV model representing a Multi-agent system (see above). The tool loads the model and starts a minimal command-line interface. Every typed ATLK formula is checked and the result of the verification is given at standard output. The command-line interface can be exited with EOF (CTRL-D).

The grammar for ATLK properties phi (under both semantics) is the following:

phi ::= EXPR | '(' phi ')' | phi '&' phi | phi '|' phi | '~'phi | phi '->' phi
        | phi '<->' phi | '<' group '>' psi | '[' GROUP ']' psi
        | 'A' psi | 'E' psi | 'nK' '<' AGENT '>' phi | 'K' '<' AGENT '>' phi
        | 'nE' '<' GROUP '>' phi | 'K' '<' GROUP '>' phi
        | 'nD' '<' GROUP '>' phi | 'D' '<' GROUP '>' phi
        | 'nC' '<' GROUP '>' phi | 'C' '<' GROUP '>' phi
psi ::= 'X' phi | 'G' phi | 'F' phi | '[' phi 'U' phi ']' | '[' phi 'W' phi ']'

where EXPR is any simple expression over variables of the system, enclosed into simple quotes (e.g. EXPR = 'transmission = completed' or EXPR = 'v = 3'), AGENT is an agent name enclosed into simple quotes, and GROUP is a comma-separated list of agent names (e.g. GROUP = 'sender', 'transmitter' or AGENT = 'dealer').


DOT model export
--------------------------------------------------------------------------------

A DOT model export tool is provided. To run this tool, run

python -m tools.dotDump model

where model is the path to an SMV model. The output of the tool is a DOT representation of the reachable state-space of the model, printed on standard output (copy/paste the output in a file or redirect sdtout into a file). This is useful to get an overview of the state-space and to inspect more precisely the model in a visual way.


Models comparator
--------------------------------------------------------------------------------

A tool to compare to NuSMV models is provided. To run this tool, run

python -m tools.compare first second

where first and second are paths to two SMV models. The output of the tool is a
comparison of both models in terms of states and transitions. The tool is
useful to compare two similar models, that is, models based on the same
set of variables but with different reachable state-space and transition
relations. The tool can, in this case, show states that are in one model but
not in another, as well as transitions that appear in one model but not in the
other.


REFERENCES
--------------------------------------------------------------------------------

[BP12] Simon Busard, Charles Pecheur: Rich Counter-Examples for Temporal-Epistemic Logic Model Checking. IWIGP 2012: 39-53
[BPQR13] Simon Busard, Charles Pecheur, Hongyang Qu, Franco Raimondi: Reasoning about Strategies under Partial Observability and Fairness Constraints. Proceedings of SR 2013, EPTCS Vol. 112, pp. 71–79, 2013.
[PL03] W.Penczek, A.Lomuscio: Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae, 55(2) :167–185, 2003.
[PR07] Charles Pecheur, Franco Raimondi: Symbolic Model Checking of Logics with Actions. MoChArt 2006: 113-128