model_checking

model_checking(primes: dict, update: str, initial_states: str, specification: str, dynamic_reorder: bool = True, disable_reachable_states: bool = True, cone_of_influence: bool = True, enable_counterexample: bool = False, enable_accepting_states: bool = False)

Calls NuSMV to check whether the specification is true or false in the transition system defined by primes, the initial_states and update. The remaining arguments are NuSMV options, see the manual at http://nusmv.fbk.eu for details.

See primes2smv and Sec. 3.4 for details on model checking with pyboolnet.

The accepting states are a dictionary with the following keywords:

  • INIT: a Boolean expression for the initial states, or None, see note below

  • INIT_SIZE: integer number of initial states, or None, see note below

  • ACCEPTING: a Boolean expression for the accepting states

  • ACCEPTING_SIZE: integer number of accepting states

  • INITACCEPTING: a Boolean expression for the intersection of initial and accepting states, or None, see note below

  • INITACCEPTING_SIZE: integer number of states in the intersection of initial and accepting states, or None, see note below

Note

disable_reachable_states is enforced as the accepting states are otherwise over-approximated.

Note

Model checking with accepting states is only possible for CTL model checking.

Note

If the ctl_spec is equivalent to either TRUE or FALSE then NuSMV will not compute the initial states, because it does not have to to find out what the answer to the query is. In that case the four values that involve the initial states are set to None.

Note

cone_of_influence is not available when using counterexamples as it “messes” with the output.

arguments:

  • primes: prime implicants

  • update: the update strategy, either “synchronous”, “asynchronous” or “mixed”

  • initial_states: a NuSMV expression for the initial states, including the keyword INIT

  • specification: a NuSMV formula, including the keyword LTLSPEC or CTLSPEC

  • dynamic_reorder: enables dynamic reordering of variables using -dynamic

  • disable_reachable_states: disables the computation of reachable states using -df

  • cone_of_influence: enables cone of influence reduction using -coi

  • enable_counterexample: enables cone of influence reduction using -coi

  • enable_accepting_states: enables cone of influence reduction using -coi

returns:

  • answer: model checking result

  • counterexample: a countereample, if enable_counterexample

  • accepting_states: the accepting states, if enable_accepting_states

example:

>>> initial_states = "INIT TRUE"
>>> update = "asynchronous"
>>> specification = "CTLSPEC AF(EG(v1&!v2))"
>>> model_checking(primes, update, initial_states, specification)
False
>>> answer, counterexample = model_checking(primes, update, initial_states, specification, enable_counterexample=True)
>>> answer, accepting_states = model_checking(primes, update, initial_states, specification, enable_accepting_states=True)
model_checking_smv_file(fname_smv: str, dynamic_reorder: bool = True, disable_reachable_states: bool = True, cone_of_influence: bool = True, enable_counterexample: bool = False, enable_accepting_states: bool = False)

Convenience function for model checking of smv files. See model_checking for details of parameters and returned objects.

primes2smv(primes: dict, update: str, initial_states, specification: str, fname_smv: Optional[str] = None) → str

Creates a NuSMV_ file from Primes and additional parameters that specify the update strategy, the initial states and the temporal logic specification.

The initial states must be defined in NuSMV syntax, i.e., starting with the keyword INIT. NuSMV uses | for disjunction, & for conjunction and ! for negation. To set the initial states to the whole state space use “INIT TRUE”. CTL formulas must start with the keyword CTLSPEC and LTL formulas with the keyword LTLSPEC.

Note

The NuSMV language is case-sensitive and does not allow single character names for variables.

Note

This function detects Boolean variables that represent multi-valued components (van Ham encoding), see StateTransitionGraphs.find_vanham_variables for details. For each multi-valued variable it adds an INIT constraint that restricts the initial states to the admissible states of the van Ham encoding.

In addition to variables that encode the activities of the components, auxillary variables are defined and available for use in CTL or LTL formulas, see Sec. 3.4 for details:

They are the Boolean name_IMAGE which is the value of the update function of the variable name in a state, the Boolean name_STEADY which is the value for whether the variable name is steady in a state, the integer SUCCESSORS which is the number of successors excluding itself (i.e., the number of variables that are changing in a state), and the Boolean STEADYSTATE which is the value for whether the current state is a steady state (which is equivalent to SUCCESSORS=0).

arguments:

  • primes: prime implicants

  • update: the update strategy, either “synchronous”, “asynchronous” or “mixed”

  • initial_states: a NuSMV expression for the initial states, including the keyword INIT

  • specification: a NuSMV formula, including the keyword LTLSPEC or CTLSPEC

  • fname_smv: name for smv file or None

returns:

  • fname_smv: file as string or None if FnameSMV is None

example:

>>> ctlspec = "CTLSPEC EF(AG(!ERK) | AG(ERK))"
>>> ltlspec = "LTLSPEC F(G(ERK))"
>>> primes2smv(primes, "asynchronous", "INIT TRUE",  ctlspec, "mapk.smv")
>>> primes2smv(primes, "synchronous",  "INIT ERK=1", ltlspec, "mapk.smv")
>>> lines = primes2smv(primes, "synchronous",  "INIT ERK=1", ltlspec)
print_warning_accepting_states_bug(primes: dict, ctl_spec: str)

This bug occurs when the Specification is equivalent to TRUE or FALSE.