void
Compile_CheckAssigns(
const SymbTable_ptr symb_table,
node_ptr procs
)
- The function checks that there are no multiple assignments and
circular definitions.
Then the functions tries to detect
multiple assignments between different modules.
void
Compile_ConstructHierarchy(
SymbLayer_ptr layer,
node_ptr module_name, the ATOM
representing the name of the
module being instantiated
node_ptr instance_name, the name of the module instance to be instantiated
node_ptr actual, the actual module arguments
FlatHierarchy_ptr result
)
- This function is a subfunction of Compile_FlattenHierarchy.
This function traverses the module hierarchy and extracts the
information needed to compile the automaton. The hierarchy of modules
is flattened, the variables are added to the symbol table, all the
necessary parts of the model are collected (i.e. the formulae to be
verified, the initial expressions, etc).
The returned value is a structure constraining all the collected parts
which are:
the list of TRANS, INIT, INVAR, ASSIGN, SPEC, COMPUTE, LTLSPEC,
PSLSPEC, INVARSPEC, JUSTICE, COMPASSION,
a full list of variables declared in the hierarchy,
a hash table associating variables to their assignments and constrains.
See FlatHierarchy class for more info.
FlatHierarchy_ptr
Compile_FlattenHierarchy(
const SymbTable_ptr symb_table,
SymbLayer_ptr layer,
node_ptr module_name,
node_ptr inst_name,
node_ptr actual,
boolean create_process_variables enables creation of process variables
)
- Traverses the module hierarchy and extracts the
information needed to compile the automaton. The hierarchy of modules
is flattened, the variables are added to the symbol table, all the
necessary parts of the model are collected (i.e. the formulae to be
verified, the initial expressions, etc). Most of the collected
expressions are flattened.
The returned value is a structure containing all the collected
parts. See FlatHierarchy_create function for more info about, and
constrains on content of the class FlatHierarchy.
NB: It is the invoker's responsibility to destroy the returned value.
NB: The parameter `create_process_variables` enables the creation of
process variable (i.e. declaration of 'running's ). So, this
parameter can be set up only for users 'main' modules. For auxiliary
modules created during execution (for example, during LTL tablaue
generation) this parameter should be set to false (as is done in ltl.c).
- Side Effects None
node_ptr
Compile_FlattenSexpExpandDefine(
const SymbTable_ptr symb_table,
node_ptr sexp,
node_ptr context
)
- Flattens an expression and expands defined symbols.
- See Also
Flatten_GetDefinition
Compile_FlattenSexp
node_ptr
Compile_FlattenSexp(
const SymbTable_ptr symb_table,
node_ptr sexp,
node_ptr context
)
- Builds the flattened version of an
expression. It does not expand defined symbols with the
corresponding body.
- See Also
Flatten_GetDefinition
Compile_FlattenSexpExpandDefine
void
Compile_ProcessHierarchy(
SymbTable_ptr symb_table,
SymbLayer_ptr layer,
FlatHierarchy_ptr hierarchy,
node_ptr name,
boolean create_process_variables
)
- This processing means:
1. process_selector variable and running defines are declared (only if
create_process_variables is on)
2. All the required lists of expressions are reversed.
All the constrains (not specifications) are flattened.
3. An association between vars and constrains are created (for ASSIGN,
INIT, INVAR, TRANS).
4. Type checking of the variable and define declarations and of all the
expressions.
5. Also a correct use of input variables and lack of circular dependenses
are checked.
The parameters:
layer is a layer with module variables.
hierachy is a hierarchy to be process.
name is a name of the module instance, i.e. a context of all expressions.
create_process_variables enables creation of process variables.
void
Compile_WriteBoolFsm(
FILE* out,
const SymbTable_ptr symb_table,
NodeList_ptr layers,
const char* fsm_name,
SexpFsm_ptr bool_sexp_fsm
)
- Prints into the specified file the boolean FSM of an
SMV model.
bool_sexp_fsm should be a boolean Sexp FSM.
layer_names is an array of layers whose variables will be printed,
usually this parameter is a list of all layers committed to enc. The array
should be ended by a NULL element.
void
Compile_WriteBoolSpecs(
FILE* out,
const SymbTable_ptr symb_table,
BddEnc_ptr enc,
node_ptr spec,
node_ptr compute,
node_ptr ltlspec,
node_ptr invarspec,
node_ptr pslspec,
node_ptr reachtarget,
node_ptr avoidtarget,
node_ptr reachdeadlock,
node_ptr avoiddeadlock,
node_ptr buchigame,
node_ptr genreactivity
)
- Prints into the specified file the flattened boolead
specifications of an SMV model.
NOTE: a temporary layer will be created during the dumping for
determinization variables that derived from the booleanization of
the specifications. These variable declarations will be printed
after the specs.
void
Compile_WriteFlattenFsm(
FILE* out,
const SymbTable_ptr symb_table,
const char** layer_names,
const char* fsm_name,
FlatHierarchy_ptr hierarchy
)
- Prints on the specified file the flatten
FSM of an SMV model, i.e. a list of all variable, defines, and all
constrains (INIT, TRANS, INVAR, ASSIGNS, JUSTICE, COMPASSION).
Specifications are NOT printed.
layer_names is an array of names of layers terminated by NULL.
fsm_name is a name of the output structure, usually it is "MODULE main".
void
Compile_WriteFlattenSpecs(
FILE* out,
const SymbTable_ptr symb_table,
node_ptr spec,
node_ptr compute,
node_ptr ltlspec,
node_ptr invarspec,
node_ptr pslspec,
node_ptr reachtarget,
node_ptr avoidtarget,
node_ptr reachdeadlock,
node_ptr avoiddeadlock,
node_ptr buchigame,
node_ptr genreactivity
)
- Prints into the specified file the flatten
specifications.
layer_names is an array of names of layers terminated by NULL.
int
Compile_check_if_bool_model_was_built(
FILE* err,
boolean forced
)
- Returns 0 if constructed, 1 otherwise. If given file is
not NULL, an error message is also printed out to it (typically, you
will use nusmv_stderr). If forced is true, thatn the model is
requested to be built even when COI is enabled.
int
Compile_check_if_encoding_was_built(
FILE* err
)
- Returns 0 if constructed, 1 otherwise. If given file is
not NULL, an error message is also printed out to it (typically, you
will use nusmv_stderr)
int
Compile_check_if_flat_model_was_built(
FILE* err,
boolean forced
)
- Returns 0 if constructed, 1 otherwise. If given file is
not NULL, an error message is also printed out to it (typically, you
will use nusmv_stderr). If forced is true, thatn the model is
requested to be built even when COI is enabled.
int
Compile_check_if_flattening_was_built(
FILE* err
)
- Returns 0 if constructed, 1 otherwise. If given file is
not NULL, an error message is also printed out to it (typically, you
will use nusmv_stderr)
int
Compile_check_if_model_was_built(
FILE* err,
boolean forced
)
- Returns 0 if constructed, 1 otherwise. If given file is
not NULL, an error message is also printed out to it (typically, you
will use nusmv_stderr). Use this function from commands that require
the model to be constructed for being executed.
void
Compile_cleanup_booleanizer_cache_about(
SymbTable_ptr st,
NodeList_ptr symbs
)
- Called by BoolEnc class when removing a layer
Expr_ptr
Compile_detexpr2bexpr(
BddEnc_ptr enc,
Expr_ptr expr
)
- Takes an scalar expression intended to evaluate
to boolean, maps through booleans down to the atomic scalar
propositions, builds the corresponding boolean function, and returns
the resulting boolean expression.
The conversion of atomic scalar proposition is currently performed
by generating the corresponding ADD, and then printing it in terms
of binary variables.
An error is returned if determinization variables are introduced in
the booleanization process.
The input expression will be processed with Nil context (for
flattened expr this does not matter).
- Side Effects None
- See Also
Compile_expr2bexpr
expr2bexpr_recur
Expr_ptr
Compile_expr2bexpr(
BddEnc_ptr enc,
SymbLayer_ptr det_layer,
Expr_ptr expr
)
- Takes an scalar expression intended to evaluate
to boolean, maps through booleans down to the atomic scalar
propositions, builds the corresponding boolean function, and returns
the resulting boolean expression.
The conversion of atomic scalar proposition is currently performed
by generating the corresponding ADD, and then printing it in terms
of binary variables.
If one or more determinization variable must be created
(i.e. non-determinism must be allowed) then det_layer is the
SymbLayer instance to be filled with the newly created
determinization variables. If non-determinism is not allowed, specify
NULL as det_layer value. In this case you can use detexpr2bexpr as well.
The input expression will be processed with Nil context (for
flattened expr this does not matter).
- Side Effects None
- See Also
Compile_detexpr2bexpr
expr2bexpr_recur
NodeList_ptr
Compile_get_expression_dependencies(
const SymbTable_ptr symb_table,
Expr_ptr expression
)
- Calls Formula_GetDependencies to get the set of
variables which appear in the expression. This is then converted to the
type NodeList_ptr and returned. It is the responsibility of the
caller to destroy the NodeList object
- Side Effects NodeList object created
FsmBuilder_ptr
Compile_get_global_fsm_builder(
)
- See fsm/FsmBuilder.h for more info
PredicateNormaliser_ptr
Compile_get_global_predicate_normaliser(
)
- See PredicateNormaliser.h for more info
on predication normaliser.
void
Compile_init_cmd(
)
- Initializes the commands provided by this package
void
Compile_init(
)
- Initializes the compile package. The set of commands must
be explicitly initialized later by calling Compile_InitCmd.
NodeList_ptr
Compile_make_sorted_vars_list_from_order(
const SymbTable_ptr st,
const NodeList_ptr vars,
const NodeList_ptr vars_order
)
- This function can be used to construct an ordered list
of symbols. The set of symbols is provided by the input list 'vars',
whereas the ordering is provided by the 'vars_order' list, that can
be an intersecting set over 'vars'. The resulting list will
contain those symbols that occur in vars_order (respecting their
order), plus all the symbols in vars that do not occur in vars_order,
pushed at the end of the list. All duplicates (if any) will not occur
into the resulting list. The returned list must be destroyed by the
caller.
node_ptr
Compile_pop_distrib_ops(
node_ptr prop
)
- Transformation rules are:
1) a :-> a
2) ( a) * ( b) :-> (a * b);
3) ( (a * b)) :-> (a * b);
4) ( ( a * b)) :-> (a * b);
5) ( ( a * b)) :-> (a * b);
Where can be either:
G|AG|H for * := &
F|AF|O for * := |
Given property can be both flattened or unflattened.
void
Compile_quit(
)
- Shut down the compile package
void
compile_check_print_io_atom_stack_assign(
FILE * fd
)
-
void
compile_create_boolean_model(
)
- The newly created layer will be committed to both the
boolean and bdd encodings. Warning: it is assumed here that the flat model
has been already created
void
compile_create_flat_model(
)
- creates the master scalar fsm if needed
node_ptr
compile_flatten_eval_number(
node_ptr n,
boolean pos
)
- Returns a NUMBER node, or Nil n is not a number.
This is a private service of function CompileFlatten_resolve_number
node_ptr
compile_flatten_resolve_name_recur(
const SymbTable_ptr symb_table,
node_ptr n,
node_ptr context
)
- Performs the recursive step of
CompileFlatten_resolve_name
.
- See Also
CompileFlatten_resolve_name
void
compile_instantiate_by_name(
SymbLayer_ptr layer,
node_ptr module_name,
node_ptr instance_name,
node_ptr actual,
node_ptr * assign,
FlatHierarchy_ptr result
)
- module_name is the name of the module being
instantiated. The name of the module instance
is instance_name. First checks if the module exists. Then it checks
if the module is recursively defined, and if the case an error is
printed out. If these checks are passed, then it proceeds in the
instantiation of the body of the module.
void
compile_instantiate_vars(
SymbLayer_ptr layer,
node_ptr var_list,
node_ptr mod_name,
node_ptr * assign,
FlatHierarchy_ptr result
)
- Recursively applies compile_instantiate_var to
a given list of variables declaration, and performs some check for
multiple variable definitions.
- See Also
compile_instantiate_var
void
compile_instantiate_var(
SymbLayer_ptr layer,
node_ptr name,
node_ptr type,
node_ptr context,
node_ptr * assign,
FlatHierarchy_ptr result
)
- It takes as input a variable and a context, and
depending on the type of the variable some operation are performed in order to
instantiate it in the given context:
- BOOLEAN
if the variable is of type boolean, then we add an entry in
symbol_hash
saying that the variable values are {0,1}
.
- RANGE
if the variable is a range of the form M..N
, then
we add an entry in the symbol_hash
saying that the
variable values are {M, M+1, ..., N-1, N}
. If
M
is less or equal to N
, than an error occurs.
- ENUMERATION
if the variable is a scalar variable whose possible values are
{a1, a2, ..., aN}
, then we add an entry in the
symbol_hash
saying that the variable values are
{a1, ..., aN}
.
- ARRAY
for each element of the array it is created the corresponding
symbol. Suppose you have the following definition "VAR
x : array 1..4 of boolean;
". We call this function
for 4 times, asking at each call i
(i
from 1
to 4) to declare the boolean variable x[i]
.
- MODULE
If the variable is an instantiation of a module, than their
arguments (if any) are contextualized, and passed as actual
parameter to instantiate_by_name with the name of the
instantiated module as root name (to extract its definition)
and as variable name as the name of the module (to perform
flattening).
- PROCESS
If the variable is of type process, than we extract the
module name and args, we perform the contextualization of the
process arguments and we perform a call to
Compile_ConstructHierarchy using the variable name as process
name (to perform flattening), the module name as root name (to
extract its definition) and the computed actual parameters.
The variables of type boolean, scalar, and array depending the kind
of variable instantiation mode are appended to
input_variables or to state_variables.
- See Also
compile_instantiate_vars
void
compile_instantiate(
SymbLayer_ptr layer,
node_ptr mod_def,
node_ptr mod_name,
node_ptr actual,
node_ptr * assign,
FlatHierarchy_ptr result
)
- This function is responsible of the
instantiation of the body of a module. The module definition
(parameter and body) is mod_def and the module instance name
mod_name are passed as arguments. First we instantiate the
arguments of the given module. Then it loops over the module
definition searching for defined symbols (i.e. those introduced by
the keyword DEFINE) and inserts their definition in the
symbol_hash. After this preliminary phase it loops again
over module body in order to performs the other instantiation, and
to extract all the information needed to compile the automaton,
i.e. the list of processes, the TRANS statements, the INIT
statements, ... and so on.
NB: After parsing and creating the module hash table, the order of
declarations is correct (not reversed). This function reverse the order
of SPEC, LTLSPEC, PSLSPEC, INVARSPEC, COMPUTE, JUSTICE AND COMPATION
- See Also
compile_instantiate_var
compile_instantiate_vars
int
compile_write_constants(
const SymbTable_ptr symb_table,
FILE* out
)
- Returns 1 if at least one char have been written, 0
otherwise
int
compile_write_flatten_bfexpr(
BddEnc_ptr enc,
const SymbTable_ptr symb_table,
SymbLayer_ptr det_layer,
FILE* out,
node_ptr n,
char* s
)
- Writes a generic expression prefixed by a given
string in SMV format on a file. The given layer is intended to hold the
determization variables that are created by the booleanization process of
the properties, that are kept not booleanized within the system.
int
compile_write_flatten_bool_vars(
const SymbTable_ptr symb_table,
const BoolEnc_ptr bool_enc,
FILE* out,
NodeList_ptr vars
)
- Writes boolean VAR and IVARS declarations in SMV format
on a file.
int
compile_write_flatten_expr_pair(
const SymbTable_ptr symb_table,
FILE* out,
node_ptr l,
char* s
)
- Writes a list of flattened expression pairs prefixed by
a given string in SMV format on a file.
int
compile_write_flatten_expr_split(
const SymbTable_ptr symb_table,
FILE* out,
node_ptr n,
char* s
)
- Writes a generic expression prefixed by a given
string in SMV format on a file.
int
compile_write_flatten_expr(
const SymbTable_ptr symb_table,
FILE* out,
node_ptr n,
char* s
)
- Writes a generic expression prefixed by a given
string in SMV format on a file.
Returns true if at least one character was printed, and false otherwise.
int
compile_write_flatten_psl(
const SymbTable_ptr symb_table,
FILE* out,
node_ptr n
)
- Writes PSL properties as they are.
int
compile_write_flatten_vars(
const SymbTable_ptr symb_table,
FILE* out,
NodeList_ptr vars
)
- Writes VAR and IVARS declarations in SMV format on a
file.