can be either:
G|AG|H for * := &
F|AF|O for * := |
Given property can be both flattened or unflattened.
void
Compile_print_array_define_udg(
FILE* out,
const node_ptr n
)
Prints a array define node to out file.
This function is exported so the hrc package can use it.
void
Compile_print_array_define(
FILE* out,
const node_ptr n
)
Prints a array define node to out file.
This function is exported so the hrc package can use it.
void
Compile_quit(
)
Shut down the compile package
void
Compile_write_dag_defines_udg(
FILE* out,
hash_ptr defines
)
void
Compile_write_dag_defines(
FILE* out,
hash_ptr defines
)
void
compile_add_vars_to_hierarhcy(
node_ptr name,
SymbType_ptr type,
FlatHierarchy_ptr fh
)
Given a fully resolved array name and its type the function
adds all the variables in the array to the hierarchy
void
compile_build_model(
boolean force_build
)
Builds the BDD fsm.
void
compile_check_print_io_atom_stack_assign(
FILE * fd
)
node_ptr
compile_cmd_get_var_type(
SymbType_ptr type
)
Creates an internal representaion of the symbol type.
The representation of the type returned is
intended to be used only with the
compile_cmd_print_type procedure. If 2 types are
the same, the same node is returned
void
compile_cmd_print_type(
FILE * file,
node_ptr ntype,
int threshold
)
Prints the given type to the given stream.
The type must be created with the
compile_cmd_get_var_type function. If the type
is scalar, then values are printed until
"threshold" number of characters are reached. If
some values are missing because of the
threshold, then "other # values" is added in
output
Expr_ptr
compile_cmd_remove_assignments(
Expr_ptr expr
)
Removes expression in the form "a := b" from the given
expression. The new expression is returned
void
compile_cmd_write_coi_prop_fsm(
FlatHierarchy_ptr fh,
Set_t cone,
Set_t props,
FILE* output_file
)
Dumps the model applied to COI for the given property
void
compile_cmd_write_coi_prop(
Set_t cone,
Set_t props,
FILE* output_file
)
Dumps the COI for the given property
void
compile_cmd_write_global_coi_fsm(
FlatHierarchy_ptr hierarchy,
Prop_Type prop_type,
FILE* output_file
)
Dumps on output_file the FSM built using the union of all
properties cone of influence. Properties can be filtered
by type using prop_type: if prop_type == Prop_NoType,
all properties are used
int
compile_cmd_write_properties_coi(
FlatHierarchy_ptr hierarchy,
Prop_Type prop_type,
boolean only_dump_coi,
const char* file_name
)
Dumps properties shared COI informations.
If only_dump_coi is true, only the set of
variables in the cone of each property is
dumped. Otherwise, an FSM is created and
dumped. Properties with the same COI will appear
in the same FSM. Properties can be filtered by
type using prop_type: if prop_type ==
Prop_NoType, all properties are used
node_ptr
compile_concat_contexts(
node_ptr ctx1,
node_ptr ctx2
)
Since contexts are organized bottom-up
("a.b.c" becomes
DOT
/ \
DOT c
/ \
a b
)
ctx2 is appended to ctx1 by concatenating ctx1 to ctx2. For example
if ctx1="c.d.e" and ctx2="a.b.c", node 'a' is searched in ctx2, and
then substituted by
/ ...
DOT
/ \
->> DOT b
/ \
(ctx1) a
Important: nodes in ctx2 are traversed and possibly recreated with find_node
node_ptr
compile_convert_to_dag_aux_udg(
SymbTable_ptr symb_table,
node_ptr expr,
hash_ptr hash,
unsigned int num_thres,
unsigned int dep_thres,
hash_ptr defines,
const char* defines_prefix
)
Private service of function Compile_convert_to_dag_udg
node_ptr
compile_convert_to_dag_aux(
SymbTable_ptr symb_table,
node_ptr expr,
hash_ptr hash,
unsigned int num_thres,
unsigned int dep_thres,
hash_ptr defines,
const char* defines_prefix
)
Private service of function Compile_convert_to_dag
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
hash_ptr
compile_create_dag_info_from_hierarchy_udg(
SymbTable_ptr st,
FlatHierarchy_ptr hierarchy,
SymbLayer_ptr det_layer,
BddEnc_ptr enc
)
If det_layer is not NULL, then hierarchy is
to be considered boolean, and specifications will be booleanized,
If det_layer is null, then also enc can be null
hash_ptr
compile_create_dag_info_from_hierarchy(
SymbTable_ptr st,
FlatHierarchy_ptr hierarchy,
SymbLayer_ptr det_layer,
BddEnc_ptr enc,
boolean force_flattening,
hash_ptr cdh
)
If det_layer is not NULL, then hierarchy is
to be considered boolean, and specifications will be booleanized,
If det_layer is null, then also enc can be null
void
compile_create_flat_model(
)
creates the master scalar fsm if needed
int
compile_encode_variables(
)
Encodes variables in the model (BDD only).
node_ptr
compile_flatten_build_word_toint_ith_bit_case(
node_ptr wexpr,
int bit,
boolean is_neg
)
Creates the following expression:
wexpr[bit:bit
node_ptr
compile_flatten_eval_number(
SymbTable_ptr st,
node_ptr n,
node_ptr context
)
This is a private service of function
CompileFlatten_resolve_number
int
compile_flatten_get_int(
node_ptr value
)
It is an error if overflow/underflow happens
node_ptr
compile_flatten_normalise_value_list(
node_ptr old_value_list
)
The normalisation includes: all TRUE and FALSE
constants are substituted by 1 and 0 numbers
node_ptr
compile_flatten_rewrite_word_toint_cast(
node_ptr body,
SymbType_ptr type
)
This functions takes a word expression and rewrites it
as a circuit in order to convert the word
expression into an integer expression.
For unsigned word[N
int
compile_flatten_smv(
boolean calc_vars_constrains
)
Traverses the parse tree coming from the smv parser and
flattens the smv file.
assoc_retval
compile_free_define_udg(
char * key,
char * data,
char * arg
)
Internal service of Compile_destroy_dag_info_udg
assoc_retval
compile_free_define(
char * key,
char * data,
char * arg
)
Internal service of Compile_destroy_dag_info
assoc_retval
compile_free_node_udg(
char * key,
char * data,
char * arg
)
Internal service of Compile_destroy_dag_info_udg
assoc_retval
compile_free_node(
char * key,
char * data,
char * arg
)
Internal service of Compile_destroy_dag_info
node_ptr
compile_get_rid_of_define_chain(
SymbTable_ptr st,
node_ptr expr,
hash_ptr cdh
)
Get rids of chain of defines until it reaches a
DEFINE whose body is not atomic (i.e. a variable, a constant, or a
complex expression). It assumes the expression being flattened.
void
compile_insert_assign_hrc(
HrcNode_ptr hrc_result,
node_ptr cur_decl
)
Add an assign declaration in hrc_result. The
type of assign is inferred by the node type found.
Side Effects Contents of hrc_result is changed adding an
assign constraint.
void
compile_instantiate_by_name(
SymbTable_ptr st,
SymbLayer_ptr layer,
node_ptr module_name,
node_ptr instance_name,
node_ptr actual,
node_ptr * assign,
FlatHierarchy_ptr result,
HrcNode_ptr hrc_result,
hash_ptr instances
)
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(
SymbTable_ptr st,
SymbLayer_ptr layer,
node_ptr var_list,
node_ptr mod_name,
node_ptr * assign,
FlatHierarchy_ptr result,
HrcNode_ptr hrc_result,
hash_ptr instances
)
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(
SymbTable_ptr st,
SymbLayer_ptr layer,
node_ptr name,
node_ptr type,
node_ptr context,
node_ptr * assign,
FlatHierarchy_ptr result,
HrcNode_ptr hrc_result,
hash_ptr instances
)
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.
Depending on the kind of variable instantiation mode the variables of
type boolean, scalar, and array are appended to input_variables,
frozen_variables or state_variables, respectively.
See Also compile_instantiate_vars
void
compile_instantiate(
SymbTable_ptr st,
SymbLayer_ptr layer,
node_ptr mod_def,
node_ptr mod_name,
node_ptr actual,
node_ptr * assign,
FlatHierarchy_ptr result,
HrcNode_ptr hrc_result,
hash_ptr instances
)
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
boolean
compile_is_booleanizable_aux(
Expr_ptr expr,
const SymbTable_ptr st,
boolean word_unbooleanizable,
hash_ptr cache
)
Private service of compile_is_booleanizable.
To represent 'true' in cache we use the constant 2 for
'false' we use 1 to avoid representation problems wrt Nil
Side Effects cache can be updated
node_ptr
compile_make_dag_info_aux_udg(
node_ptr expr,
hash_ptr hash
)
Returns a node COLON(NUMBER count, NUMBER depth)
node_ptr
compile_make_dag_info_aux(
node_ptr expr,
hash_ptr hash
)
Returns a node COLON(NUMBER count, NUMBER depth)
node_ptr
compile_pack_dag_info_udg(
unsigned int count,
unsigned int depth
)
Packs given count and depth into a node
node_ptr
compile_pack_dag_info(
unsigned int count,
unsigned int depth,
boolean admissible
)
Packs given count and depth into a node
void
compile_print_assign_udg(
SymbTable_ptr st,
FILE * out,
node_ptr lhs,
node_ptr rhs,
hash_ptr dag_info,
hash_ptr defines
)
Prints an assignement statement
void
compile_print_assign(
SymbTable_ptr st,
FILE * out,
node_ptr lhs,
node_ptr rhs,
hash_ptr dag_info,
hash_ptr defines
)
Prints an assignement statement
void
compile_set_dag_info_udg(
node_ptr info,
unsigned int count,
unsigned int depth
)
Sets count and depth
void
compile_set_dag_info(
node_ptr info,
unsigned int count,
unsigned int depth,
boolean admissible
)
Sets count and depth
void
compile_symbtype_obfuscated_print(
SymbType_ptr type,
FILE* out,
const SymbTable_ptr symb_table,
hash_ptr obfuscation_map
)
Prints the obfuscation of the given type
void
compile_unpack_dag_info_udg(
node_ptr info,
unsigned int* count,
unsigned int* depth
)
Unpacks given node to count and deptch
void
compile_unpack_dag_info(
node_ptr info,
unsigned int* count,
unsigned int* depth,
boolean* admissible
)
Unpacks given node to count and deptch
void
compile_write_bool_fsm(
FILE* out,
const SymbTable_ptr symb_table,
NodeList_ptr layers,
const char* fsm_name,
BoolSexpFsm_ptr bool_sexp_fsm,
hash_ptr dag_info,
hash_ptr defines,
boolean force_flattening,
hash_ptr cdh
)
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_write_bool_specs(
FILE* out,
BddEnc_ptr enc,
SymbLayer_ptr det_layer,
FlatHierarchy_ptr hierarchy,
hash_ptr dag_info,
hash_ptr defines,
hash_ptr cdh
)
Prints into the specified file the booleanized
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_write_bool_spec(
FILE* out,
BddEnc_ptr enc,
node_ptr spec,
const char* msg,
SymbLayer_ptr det_layer,
hash_ptr dag_info,
hash_ptr defines,
hash_ptr cdh
)
Private service to print a boolean specification
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_flat_array_define_udg(
const SymbTable_ptr symb_table,
FILE* out,
const NodeList_ptr names,
hash_ptr dag_info,
hash_ptr defines
)
Writes ARRAY DEFINE declarations in SMV format on a
file.
int
compile_write_flat_asgn(
const SymbTable_ptr symb_table,
FILE* out,
const NodeList_ptr vars,
FlatHierarchy_ptr hierarchy,
hash_ptr dag_info,
hash_ptr defines,
hash_ptr cdh
)
Writes flattened ASSIGN declarations in SMV format on a
file.
int
compile_write_flat_define_aux(
const SymbTable_ptr symb_table,
FILE* out,
node_ptr name,
hash_ptr dag_info,
hash_ptr defines,
hash_ptr printed_arrays,
boolean force_flattening
)
If a define happens to be an array define's element
then array is output (and remembered in printed_arrays)
instead of the original identifiers.
int
compile_write_flat_define(
const SymbTable_ptr symb_table,
FILE* out,
const NodeList_ptr names,
hash_ptr dag_info,
hash_ptr defines,
boolean force_flattening
)
Writes DEFINE declarations in SMV format on a file.
void
compile_write_flat_fsm(
FILE* out,
const SymbTable_ptr symb_table,
const array_t* layer_names,
const char* fsm_name,
FlatHierarchy_ptr hierarchy,
hash_ptr dag_info,
hash_ptr defines,
boolean force_flattening,
hash_ptr cdh
)
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 that is typically
obtained from the symbol table. fsm_name is a name of the output
structure, usually it is "MODULE main".
void
compile_write_flat_specs(
FILE* out,
const SymbTable_ptr st,
FlatHierarchy_ptr hierarchy,
hash_ptr dag_info,
hash_ptr defines,
boolean force_flattening,
hash_ptr cdh
)
Prints into the specified file the
specifications of an SMV model.
void
compile_write_flat_spec(
FILE* out,
const SymbTable_ptr symb_table,
node_ptr spec,
const char* msg,
hash_ptr dag_info,
hash_ptr defines,
boolean force_flattening,
hash_ptr cdh
)
Prints into the specified file the flatten
specifications.
int
compile_write_flatten_bfexpr(
BddEnc_ptr enc,
const SymbTable_ptr symb_table,
SymbLayer_ptr det_layer,
FILE* out,
node_ptr n,
const char* s,
hash_ptr dag_info,
hash_ptr defines,
hash_ptr cdh
)
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, FROZENVAR and IVAR declarations in
SMV format on a file. Non boolean vars are dumped as defines for the sake of
readability of conterexamples.
int
compile_write_flatten_expr_pair(
const SymbTable_ptr symb_table,
FILE* out,
node_ptr l,
const char* s,
hash_ptr dag_info,
hash_ptr defines,
boolean force_flattening,
hash_ptr cdh
)
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,
const char* s,
hash_ptr dag_info,
hash_ptr defines,
boolean force_flattening,
hash_ptr cdh
)
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,
const char* s,
hash_ptr dag_info,
hash_ptr defines,
boolean force_flattening,
hash_ptr cdh
)
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,
hash_ptr dag_info,
hash_ptr defines,
hash_ptr cdh
)
Writes PSL properties as they are.
int
compile_write_flatten_spec_split(
const SymbTable_ptr symb_table,
FILE* out,
node_ptr n,
const char* s,
hash_ptr dag_info,
hash_ptr defines,
boolean force_flattening,
hash_ptr cdh
)
Writes a generic spec prefixed by a given
string in SMV format on a file.
int
compile_write_flatten_spec(
const SymbTable_ptr symb_table,
FILE* out,
node_ptr n,
const char* s,
hash_ptr dag_info,
hash_ptr defines,
boolean force_flattening,
hash_ptr cdh
)
Writes a generic spec 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_vars_aux(
const SymbTable_ptr symb_table,
const node_ptr name,
FILE* out,
hash_ptr printed
)
If the identifier contains an index subscript in its
name then at first the identifier check for being a part of an array.
In this case array is output (and remembered in "printed") instead of
the var. Otherwise, the identifier is output.
int
compile_write_flatten_vars(
const SymbTable_ptr symb_table,
FILE* out,
NodeList_ptr vars
)
Writes VAR, FROZENVAR, and IVAR declarations in
SMV format on a file.
NodeList_ptr
compile_write_get_restricted_vars(
Set_t keep_vars,
NodeList_ptr all_vars
)
Processes the intersection between the given set
and the given list
int
compile_write_obfuscated_constants(
const SymbTable_ptr symb_table,
FILE* out,
hash_ptr obfuscation_map
)
Returns 1 if at least one char have been written, 0
otherwise
void
compile_write_obfuscated_dag_defines(
FILE* out,
const SymbTable_ptr st,
hash_ptr defines,
hash_ptr obfuscation_map
)
int
compile_write_obfuscated_flat_asgn(
const SymbTable_ptr symb_table,
FILE* out,
const NodeList_ptr vars,
FlatHierarchy_ptr hierarchy,
hash_ptr dag_info,
hash_ptr defines,
hash_ptr obfuscation_map,
hash_ptr cdh
)
Writes flattened ASSIGN declarations in SMV format on a
file.
int
compile_write_obfuscated_flat_define_aux(
const SymbTable_ptr symb_table,
FILE* out,
node_ptr name,
hash_ptr dag_info,
hash_ptr defines,
hash_ptr printed_arrays,
hash_ptr obfuscation_map,
boolean force_flattening
)
This function behaves example like
compile_write_flat_define_aux
except that identifiers are obfuscated before being printed.
See Also compile_write_flat_define_aux
int
compile_write_obfuscated_flat_define(
const SymbTable_ptr symb_table,
FILE* out,
const NodeList_ptr names,
hash_ptr dag_info,
hash_ptr defines,
hash_ptr obfuscation_map,
boolean force_flattening
)
This function behaves exactly like compile_write_flat_define
except that identifiers a re obfuscated before.
void
compile_write_obfuscated_flat_fsm(
FILE* out,
const SymbTable_ptr symb_table,
const array_t* layer_names,
const char* fsm_name,
FlatHierarchy_ptr hierarchy,
hash_ptr dag_info,
hash_ptr defines,
hash_ptr obfuscation_map,
boolean force_flattening,
hash_ptr cdh
)
Prints the obfuscated flatten version of FSM of an
SMV model.
See Also compile_write_flat_fsm
void
compile_write_obfuscated_flat_specs(
FILE* out,
const SymbTable_ptr st,
FlatHierarchy_ptr hierarchy,
hash_ptr dag_info,
hash_ptr defines,
hash_ptr obfuscation_map,
boolean force_flattening,
hash_ptr cdh
)
Prints the obfuscated flatten specifications of an
SMV model.
See Also compile_write_flat_specs
void
compile_write_obfuscated_flat_spec(
FILE* out,
const SymbTable_ptr symb_table,
node_ptr spec,
const char* msg,
hash_ptr dag_info,
hash_ptr defines,
hash_ptr obfuscation_map,
boolean force_flattening,
hash_ptr cdh
)
Prints into the specified file the flatten
specifications.
int
compile_write_obfuscated_flatten_expr_pair(
const SymbTable_ptr symb_table,
FILE* out,
node_ptr l,
const char* s,
hash_ptr dag_info,
hash_ptr defines,
hash_ptr obfuscation_map,
boolean force_flattening,
hash_ptr cdh
)
Writes a list of flattened expression pairs prefixed by
a given string in SMV format on a file.
int
compile_write_obfuscated_flatten_expr_split(
const SymbTable_ptr symb_table,
FILE* out,
node_ptr n,
const char* s,
hash_ptr dag_info,
hash_ptr defines,
hash_ptr obfuscation_map,
boolean force_flattening,
hash_ptr cdh
)
Writes a generic expression prefixed by a given
string in SMV format on a file.
int
compile_write_obfuscated_flatten_expr(
const SymbTable_ptr symb_table,
FILE* out,
node_ptr n,
const char* s,
hash_ptr dag_info,
hash_ptr defines,
hash_ptr obfuscation_map,
boolean force_flattening,
hash_ptr cdh
)
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_obfuscated_flatten_spec_split(
const SymbTable_ptr symb_table,
FILE* out,
node_ptr n,
const char* s,
hash_ptr dag_info,
hash_ptr defines,
hash_ptr obfuscation_map,
boolean force_flattening,
hash_ptr cdh
)
Writes a generic spec prefixed by a given
string in SMV format on a file.
int
compile_write_obfuscated_flatten_spec(
const SymbTable_ptr symb_table,
FILE* out,
node_ptr n,
const char* s,
hash_ptr dag_info,
hash_ptr defines,
hash_ptr obfuscation_map,
boolean force_flattening,
hash_ptr cdh
)
Writes a generic spec prefixed by a given
string in SMV format on a file.
Returns true if at least one character was printed, and false otherwise.
boolean
compile_write_obfuscated_flatten_vars_aux(
const SymbTable_ptr symb_table,
const node_ptr name,
FILE* out,
hash_ptr printed,
hash_ptr obfuscation_map
)
The function works exactly like
compile_write_flatten_vars_aux but all identifiers
are obfuscated before being printed.
See Also compile_write_flatten_vars_aux
int
compile_write_obfuscated_flatten_vars(
const SymbTable_ptr symb_table,
FILE* out,
NodeList_ptr vars,
hash_ptr obfuscation_map
)
Writes VAR, FROZENVAR, and IVAR declarations in
SMV format on a file.
void
compile_write_restricted_flat_fsm(
FILE* out,
const SymbTable_ptr symb_table,
const array_t* layer_names,
const char* fsm_name,
FlatHierarchy_ptr hierarchy,
hash_ptr dag_info,
hash_ptr defines,
boolean force_flattening,
hash_ptr cdh
)
Prints on the specified file the flatten
FSM of an SMV model, i.e. a list of restricted variables, defines, and all
constrains (INIT, TRANS, INVAR, ASSIGNS, JUSTICE, COMPASSION) restricted to
the set of variables in the FlatHierarchy.
Specifications are NOT printed.
layer_names is an array of names of layers that is typically
obtained from the symbol table. fsm_name is a name of the output
structure, usually it is "MODULE main".
void
compile_write_udg_bool_fsm(
FILE* out,
const SymbTable_ptr symb_table,
NodeList_ptr layers,
const char* fsm_name,
BoolSexpFsm_ptr bool_sexp_fsm,
hash_ptr dag_info,
hash_ptr defines
)
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_write_udg_bool_specs(
FILE* out,
BddEnc_ptr enc,
SymbLayer_ptr det_layer,
FlatHierarchy_ptr hierarchy,
hash_ptr dag_info,
hash_ptr defines
)
Prints into the specified file the booleanized
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_write_udg_bool_spec(
FILE* out,
BddEnc_ptr enc,
node_ptr spec,
const char* msg,
SymbLayer_ptr det_layer,
hash_ptr dag_info,
hash_ptr defines
)
Private service to print a boolean specification
int
compile_write_udg_constants(
const SymbTable_ptr symb_table,
FILE* out
)
Returns 1 if at least one char have been written, 0
otherwise
int
compile_write_udg_flat_asgn(
const SymbTable_ptr symb_table,
FILE* out,
const NodeList_ptr vars,
FlatHierarchy_ptr hierarchy,
hash_ptr dag_info,
hash_ptr defines
)
Writes flattened ASSIGN declarations in SMV format on a
file.
int
compile_write_udg_flat_define(
const SymbTable_ptr symb_table,
FILE* out,
const NodeList_ptr names,
hash_ptr dag_info,
hash_ptr defines
)
Writes DEFINE declarations in SMV format on a
file.
void
compile_write_udg_flat_fsm(
FILE* out,
const SymbTable_ptr symb_table,
const array_t* layer_names,
const char* fsm_name,
FlatHierarchy_ptr hierarchy,
hash_ptr dag_info,
hash_ptr defines
)
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 that is typically
obtained from the symbol table. fsm_name is a name of the output
structure, usually it is "MODULE main".
void
compile_write_udg_flat_specs(
FILE* out,
const SymbTable_ptr st,
FlatHierarchy_ptr hierarchy,
hash_ptr dag_info,
hash_ptr defines
)
Prints into the specified file the
specifications of an SMV model.
node_ptr
compile_write_udg_flatten_array_define(
SymbTable_ptr st,
node_ptr body,
node_ptr context
)
Writes DEFINE declarations in SMV format on a
file.
int
compile_write_udg_flatten_bfexpr(
BddEnc_ptr enc,
const SymbTable_ptr symb_table,
SymbLayer_ptr det_layer,
FILE* out,
node_ptr n,
const char* s,
hash_ptr dag_info,
hash_ptr defines
)
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_udg_flatten_bool_vars(
const SymbTable_ptr symb_table,
const BoolEnc_ptr bool_enc,
FILE* out,
NodeList_ptr vars
)
Writes boolean VAR, FROZENVAR and IVAR declarations in
SMV format on a file. Non boolean vars are dumped as defines for the sake of
readability of conterexamples.
int
compile_write_udg_flatten_expr_pair(
const SymbTable_ptr symb_table,
FILE* out,
node_ptr l,
ModelSectionTag mst,
hash_ptr dag_info,
hash_ptr defines
)
Writes a list of flattened expression pairs prefixed by
a given string in SMV format on a file.
int
compile_write_udg_flatten_expr_split(
const SymbTable_ptr symb_table,
FILE* out,
node_ptr n,
ModelSectionTag mst,
hash_ptr dag_info,
hash_ptr defines
)
Writes a generic expression prefixed by a given
string in SMV format on a file.
int
compile_write_udg_flatten_expr(
const SymbTable_ptr symb_table,
FILE* out,
node_ptr n,
ModelSectionTag mst,
hash_ptr dag_info,
hash_ptr defines
)
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_udg_flatten_psl(
const SymbTable_ptr symb_table,
FILE* out,
node_ptr n,
hash_ptr dag_info,
hash_ptr defines
)
Writes PSL properties as they are.
int
compile_write_udg_flatten_spec_split(
const SymbTable_ptr symb_table,
FILE* out,
node_ptr n,
ModelSectionTag mst,
hash_ptr dag_info,
hash_ptr defines
)
Writes a generic spec prefixed by a given
string in SMV format on a file.
int
compile_write_udg_flatten_spec(
const SymbTable_ptr symb_table,
FILE* out,
node_ptr n,
ModelSectionTag mst,
hash_ptr dag_info,
hash_ptr defines
)
Writes a generic spec 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_udg_flatten_vars(
const SymbTable_ptr symb_table,
FILE* out,
NodeList_ptr vars
)
Writes VAR, FROZENVAR, and IVAR declarations in
SMV format on a file.
inline int
compile_write_udg_print_1_ary(
FILE* buffer,
node_ptr code,
const char* str,
boolean close,
boolean shared,
const char* color1
)
Printer in udg format for a node with a child
inline int
compile_write_udg_print_2_arya(
FILE* buffer,
node_ptr code,
const char* str,
boolean close,
boolean shared
)
Printer in udg format for a node with children arity equal to 2
inline int
compile_write_udg_print_2_ary(
FILE* buffer,
node_ptr code,
const char* str,
boolean close,
boolean shared,
const char* color1,
const char* color2
)
Printer in udg format for a node with children arity equal to 2
inline int
compile_write_udg_print_3_aryc_color(
FILE* buffer,
node_ptr code,
const char* str,
node_ptr fst,
node_ptr snd,
node_ptr trd,
boolean close,
boolean shared,
const char* color1,
const char* color2,
const char* color3
)
The children are provided explicitly
inline int
compile_write_udg_print_3_aryc(
FILE* buffer,
node_ptr code,
const char* str,
node_ptr fst,
node_ptr snd,
node_ptr trd,
boolean close,
boolean shared
)
The children are provided explicitly
int
compile_write_udg_print_node(
FILE* out,
node_ptr n,
boolean close,
boolean shared,
const char* style
)
Menthod that prints the given node in udg format