NuSMV export

Each variable is declared under the VAR section together with the corresponding range of values (domain). The order of the declaration of variables is of extreme importance since it influences the construction of the internal BDD representing the whole dynamics.

The initialization of a set of variables is performed by using the INIT keyword followed by an assignment of a value to a given variable. Alternatively, a macro can be defined with a conjunction of variable valuations and simply use the macro name with the INIT keyword.

The rules concerning the computation of the target value of a given variable are described under the ASSIGN section, using the next(Var) := ...; form.

The computation of the focal point is declared under the DEFINE section, where the actual logical rules referencing all the regulatory components are declared. In this section it is also declared all the macros to be used in the property specifications, such as weak and strong stable states, the list of initial conditions defined by the user, or the output variables which (if specified) do not participate in the state characterization.

In this export, all of the possible updating policies synchronous/asynchronous are considered as being special cases of the priority classes:

There are three main types of variables characterizing a state: state variables, which are declared under the VAR section; output variables, which (if specified by the "Strip outputs" option) are declared as macros under the DEFINE section; and the input variables, which are declared under the IVAR section.

State variables are the ones characterizing an internal state in NuSMV, so, whenever one of the state variables is called to change, a new successor is (might be) created. Output variables are the ones that are not critical for the state characterization, and whose values can be computed through state variables alone. Output variables can still be referenced with a temporal operator in a property specification though. Input variables are always projected over transitions rather then the state. Between a state and its successor, a transition contains all the valid input valuations, i.e., if a given input valuation does not permit to follow a given transition is will be not represented over that transition.

The NuSMV export will always automatically compute the model stable states and insert them in the NuSMV model description. Every stableState is either a weakSS or a strongSS, and each one of these can be composed by several ones, depending on the model. The user, can then use each of these macro names for the specification of properties, from a general one stableState to a more specific one strongSS.

Additionally, when exporting a model, the user can define and select state restrictions on the internal components or on the input components. Only the ones that are checked will be written on the NuSMV specification. Similarly, the names given to each of these state restrictions will correspond to macro names which can be used in the specification of properties.

This NuSMV specification of the logical model, does not include any property specifications. It is up to the user to encode them at the end of the NuSMV specification file. Again, in any given property, the user can always use the stableState or the initialStateList macros previously defined. In order to aid the user in such task, the following example reachability properties are added, as comments, at the end of each file.

--------------------------------------------------
-- Reachability Properties using VARYING INPUTS --
-- i.e. there is NO CONTROL on the input change at each transition
--
-- 1. Between an initial state (pattern) and a stable state (pattern)
--   a. Existence of at least one path connecting two state patterns
-- INIT initState;
-- SPEC EF ( stableState );
--   b. Existence of all the paths connecting two state patterns
-- INIT initState;
-- SPEC AF ( stableState );
--
-- 2. Between all the weak/strong stable states
-- INIT weakSS1;
--  SPEC EF ( weakSS2 );
--  ...
--  SPEC EF ( weakSSn );
--------------------------------------------------
-- Reachability Properties using FIXED INPUTS --
-- i.e. a VALUE RESTRICTION can be forced at each transition
-- 
-- 1. Between an initial state (pattern) and a stable state (pattern)
--   a. Existence of at least one path connecting two state patterns
-- INIT initState; SPEC EAF ( inpVar1=0 & inpVar3=1 )( stableState );
--   b. Existence of all the paths
-- INIT initState; SPEC AAF ( inpVar1=0 & inpVar3=1 )( stableState );
--
-- 2. Testing input combinations
-- INIT weakSS1;
--  SPEC EAF ( inpVar1=0 & inpVar2=0 )( weakSS2 );
--  SPEC EAF ( inpVar1=0 & inpVar2=1 )( weakSS2 );
--  SPEC EAF ( inpVar1=1 & inpVar2=0 )( weakSS2 );
--  SPEC EAF ( inpVar1=1 & inpVar2=1 )( weakSS2 );
--  ...

This export was implemented in GINsim 3.0. Further information is available in Monteiro and Chaouiya (PACBB 2012).