int CommandBuildBooleanModel( int argc, char ** argv )
compileCmd.c
int CommandBuildFlatModel( int argc, char ** argv )
compileCmd.c
int CommandBuildModel( int argc, char ** argv )
compileCmd.c
int CommandCPPrintClusterInfo( int argc, char ** argv )
compileCmd.c
int CommandEncodeVariables( int argc, char ** argv )
compileCmd.c
int CommandFlattenHierarchy( int argc, char ** argv )
compileCmd.c
int CommandGetInternalStatus( int argc, char ** argv )
compileCmd.c
int CommandGoBmc( int argc, char ** argv )
compileCmd.c
int CommandGo( int argc, char ** argv )
compileCmd.c
int CommandIwls95PrintOption( int argc, char ** argv )
compileCmd.c
int CommandPrintFsmStats( int argc, char ** argv )
compileCmd.c
int CommandProcessModel( int argc, char ** argv )
compileCmd.c
int CommandShowVars( int argc, char ** argv )
compileCmd.c
int CommandWriteModelFlatBool( int argc, char ** argv )
compileCmd.c
int CommandWriteModelFlat( int argc, char ** argv )
compileCmd.c
int CommandWriteOrder( int argc, char ** argv )
compileCmd.c
node_ptr CompileFlatten_expand_range( int a, int b )
compileFlatten.c
void CompileFlatten_init_flattener( )
compileFlatten.c
node_ptr CompileFlatten_normalise_value_list( node_ptr old_value_list )
compileFlatten.c
void CompileFlatten_quit_flattener( )
compileFlatten.c
node_ptr CompileFlatten_resolve_name( const SymbTable_ptr symb_table, node_ptr name, node_ptr context )
n
in
module instance context
. If the given symbol is a formal
parameter of the module instance, than the actual parameter is
built. If the given symbol is an array, than the expression
referring to the element of the array must evaluate to an unique
integer (not to a set of integers) in the range of array bound.
NULL is returned if the given expression is not syntactically an
identifier.
NOTE: param symb_table is used only when the name is an array whose
index is not a constant number. If the caller is sure that this is
not the case, it is possible to pass NULL instead.
compile_flatten_resolve_name_recur
compileFlatten.c
node_ptr CompileFlatten_resolve_number( SymbTable_ptr symb_table, node_ptr n, node_ptr context )
compileFlatten.c
void Compile_CheckAssigns( const SymbTable_ptr symb_table, node_ptr procs )
compileCheck.c
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
)
compileFlatten.c
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 )
compileFlatten.c
node_ptr Compile_FlattenSexpExpandDefine( const SymbTable_ptr symb_table, node_ptr sexp, node_ptr context )
Flatten_GetDefinition
Compile_FlattenSexp
compileFlatten.c
node_ptr Compile_FlattenSexp( const SymbTable_ptr symb_table, node_ptr sexp, node_ptr context )
Flatten_GetDefinition
Compile_FlattenSexpExpandDefine
compileFlatten.c
void Compile_ProcessHierarchy( SymbTable_ptr symb_table, SymbLayer_ptr layer, FlatHierarchy_ptr hierarchy, node_ptr name, boolean create_process_variables )
compileFlatten.c
void Compile_WriteBoolFsm( FILE* out, const SymbTable_ptr symb_table, NodeList_ptr layers, const char* fsm_name, SexpFsm_ptr bool_sexp_fsm )
compileWrite.c
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 )
compileWrite.c
void Compile_WriteFlattenFsm( FILE* out, const SymbTable_ptr symb_table, const char** layer_names, const char* fsm_name, FlatHierarchy_ptr hierarchy )
compileWrite.c
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 )
compileWrite.c
int Compile_check_if_bool_model_was_built( FILE* err, boolean forced )
compileUtil.c
int Compile_check_if_encoding_was_built( FILE* err )
compileUtil.c
int Compile_check_if_flat_model_was_built( FILE* err, boolean forced )
compileUtil.c
int Compile_check_if_flattening_was_built( FILE* err )
compileUtil.c
int Compile_check_if_model_was_built( FILE* err, boolean forced )
compileUtil.c
void Compile_cleanup_booleanizer_cache_about( SymbTable_ptr st, NodeList_ptr symbs )
compileBEval.c
Expr_ptr Compile_detexpr2bexpr( BddEnc_ptr enc, Expr_ptr expr )
Compile_expr2bexpr
expr2bexpr_recur
compileBEval.c
Expr_ptr Compile_expr2bexpr( BddEnc_ptr enc, SymbLayer_ptr det_layer, Expr_ptr expr )
Compile_detexpr2bexpr
expr2bexpr_recur
compileBEval.c
NodeList_ptr Compile_get_expression_dependencies( const SymbTable_ptr symb_table, Expr_ptr expression )
compileCheck.c
FsmBuilder_ptr Compile_get_global_fsm_builder( )
compileStruct.c
PredicateNormaliser_ptr Compile_get_global_predicate_normaliser( )
compileStruct.c
void Compile_init_cmd( )
compileCmd.c
void Compile_init( )
compileCmd.c
NodeList_ptr Compile_make_sorted_vars_list_from_order( const SymbTable_ptr st, const NodeList_ptr vars, const NodeList_ptr vars_order )
compileUtil.c
node_ptr Compile_pop_distrib_ops( node_ptr prop )
compileUtil.c
void Compile_quit( )
compileCmd.c
Set_t ComputeCOI( const SymbTable_ptr symb_table, Set_t base )
compileCone.c
node_ptr Flatten_GetDefinition( const SymbTable_ptr symb_table, node_ptr atom )
compileFlatten.c
void Flatten_remove_symbol_info( node_ptr name )
compileFlatten.c
Set_t Formula_GetDependenciesByType( const SymbTable_ptr symb_table, node_ptr formula, node_ptr context, VarFilterType filter )
formulaGetDependenciesByTypeAux
formulaGetDefinitionDependencies
compileCone.c
Set_t Formula_GetDependencies( const SymbTable_ptr symb_table, node_ptr formula, node_ptr context )
formulaGetDefinitionDependencies
compileCone.c
Set_t Formulae_GetDependencies( const SymbTable_ptr symb_table, node_ptr formula, node_ptr justice, node_ptr compassion )
compileCone.c
static void check_assign_both( node_ptr v, int node_type, int lineno )
compileCheck.c
static void check_assign( const SymbTable_ptr symb_table, node_ptr n, node_ptr context, int mode )
compileCheck.c
static void check_circular_assign( const SymbTable_ptr symb_table, node_ptr n, node_ptr context, boolean is_next, boolean is_lhs, boolean lhs_is_next )
compileCheck.c
static void check_circ( const SymbTable_ptr symb_table, node_ptr n, node_ptr context, boolean is_next, boolean lhs_is_next )
next(x) := alpha(next(x))
next(x) := next(alpha(x))
x := alpha(x)
alpha(x)
(alpha(next(x))
) is a
formula in which the variable x
(next(x)
)
occurs. Notice that next(alpha(x))
can be rewritten in
term of next(x)
, since the next operator distributes
along all kind of operators.
compileCheck.c
cmp_struct_ptr cmp_struct_init( )
compileStruct.c
static void coiInit( const SymbTable_ptr symb_table, FlatHierarchy_ptr hierarchy )
ComputeCOI
compileCone.c
void compileCheckAssignForInputVars( SymbTable_ptr symb_table, node_ptr assign, FlatHierarchy_ptr hierarchy )
compileCheck.c
void compileCheckForInputVars( const SymbTable_ptr symb_table, node_ptr trans_expr, node_ptr init_expr, node_ptr invar_expr, node_ptr assign_expr, FlatHierarchy_ptr hierarchy )
compileCheck.c
void compileCheckInitForInputVars( SymbTable_ptr symb_table, node_ptr init )
compileCheck.c
void compileCheckInvarForInputVars( SymbTable_ptr symb_table, node_ptr invar )
compileCheck.c
void compileCheckTransForInputVars( SymbTable_ptr symb_table, node_ptr trans )
compileCheck.c
boolean compileExpressionHasNextInputs( SymbTable_ptr symb_table, node_ptr expr )
compileCheck.c
static Set_t compileFlattenConstantSexpCheck( const SymbLayer_ptr layer, node_ptr expr, int type )
optional
compileFlatten.c
static void compileFlattenProcessRecur( const SymbTable_ptr symb_table, node_ptr assign, node_ptr context, node_ptr running, FlatHierarchy_ptr flatHierarchy )
compileFlatten.c
static node_ptr compileFlattenProcess( const SymbTable_ptr symb_table, node_ptr proc_assign_list, FlatHierarchy_ptr flattenHierarchy )
compileFlatten.c
static void compileFlattenSexpModelAux( const SymbTable_ptr symb_table, const SymbLayer_ptr layer, node_ptr expr, int type, FlatHierarchy_ptr flatHierarchy )
compileFlatten.c
static void compileFlattenSexpModelRecur( const SymbTable_ptr symb_table, const SymbLayer_ptr layer, node_ptr expr, int type, FlatHierarchy_ptr flatHierarchy )
compileFlatten.c
static void compileFlattenSexpModel( const SymbTable_ptr symb_table, const SymbLayer_ptr layer, node_ptr init_expr, node_ptr invar_expr, node_ptr trans_expr, FlatHierarchy_ptr flatHierarchy )
compileFlattenProcess
compileFlatten.c
static node_ptr compileFlattenSexpRecur( const SymbTable_ptr symb_table, node_ptr sexp, node_ptr context )
Compile_FlattenSexp
Compile_FlattenSexpExpandDefine
compileFlatten.c
void compile_check_print_io_atom_stack_assign( FILE * fd )
compileCheck.c
void compile_create_boolean_model( )
compileCmd.c
void compile_create_flat_model( )
compileCmd.c
node_ptr compile_flatten_eval_number( node_ptr n, boolean pos )
compileFlatten.c
node_ptr compile_flatten_resolve_name_recur( const SymbTable_ptr symb_table, node_ptr n, node_ptr context )
CompileFlatten_resolve_name
.
CompileFlatten_resolve_name
compileFlatten.c
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 )
compileFlatten.c
void compile_instantiate_vars( SymbLayer_ptr layer, node_ptr var_list, node_ptr mod_name, node_ptr * assign, FlatHierarchy_ptr result )
compile_instantiate_var
compileFlatten.c
void compile_instantiate_var( SymbLayer_ptr layer, node_ptr name, node_ptr type, node_ptr context, node_ptr * assign, FlatHierarchy_ptr result )
symbol_hash
saying that the variable values are {0,1}
.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.{a1, a2, ..., aN}
, then we add an entry in the
symbol_hash
saying that the variable values are
{a1, ..., aN}
. 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]
.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).
compile_instantiate_vars
compileFlatten.c
void compile_instantiate( SymbLayer_ptr layer, node_ptr mod_def, node_ptr mod_name, node_ptr actual, node_ptr * assign, FlatHierarchy_ptr result )
compile_instantiate_var
compile_instantiate_vars
compileFlatten.c
int compile_write_constants( const SymbTable_ptr symb_table, FILE* out )
compileWrite.c
int compile_write_flatten_bfexpr( BddEnc_ptr enc, const SymbTable_ptr symb_table, SymbLayer_ptr det_layer, FILE* out, node_ptr n, char* s )
compileWrite.c
int compile_write_flatten_bool_vars( const SymbTable_ptr symb_table, const BoolEnc_ptr bool_enc, FILE* out, NodeList_ptr vars )
compileWrite.c
int compile_write_flatten_expr_pair( const SymbTable_ptr symb_table, FILE* out, node_ptr l, char* s )
compileWrite.c
int compile_write_flatten_expr_split( const SymbTable_ptr symb_table, FILE* out, node_ptr n, char* s )
compileWrite.c
int compile_write_flatten_expr( const SymbTable_ptr symb_table, FILE* out, node_ptr n, char* s )
compileWrite.c
int compile_write_flatten_psl( const SymbTable_ptr symb_table, FILE* out, node_ptr n )
compileWrite.c
int compile_write_flatten_vars( const SymbTable_ptr symb_table, FILE* out, NodeList_ptr vars )
compileWrite.c
static void create_process_symbolic_variables( SymbTable_ptr symb_table, SymbLayer_ptr layer, node_ptr process_name_list )
compileFlatten.c
void error_bit_selection_assignment_not_supported( node_ptr name )
compileFlatten.c
static node_ptr expr2bexpr_get_shift_def_value( BddEnc_ptr enc, SymbLayer_ptr det_layer, node_ptr context, boolean in_next, node_ptr a, node_ptr b, int wb )
compileBEval.c
static node_ptr expr2bexpr_ite( BddEnc_ptr enc, SymbLayer_ptr det_layer, node_ptr expr, node_ptr context, boolean in_next )
expr2bexpr_word_ite_aux
compileBEval.c
static node_ptr expr2bexpr_recur_binary( BddEnc_ptr enc, SymbLayer_ptr det_layer, node_ptr expr, node_ptr context, boolean in_next, NPFNN op )
compileBEval.c
static node_ptr expr2bexpr_recur_unary( BddEnc_ptr enc, SymbLayer_ptr det_layer, node_ptr expr, node_ptr context, boolean in_next, NPFN op )
compileBEval.c
static node_ptr expr2bexpr_recur( BddEnc_ptr enc, SymbLayer_ptr det_layer, node_ptr expr, node_ptr context, boolean in_next )
Compile_expr2bexpr
detexpr2bexpr
compileBEval.c
static node_ptr expr2bexpr_rotate( BddEnc_ptr enc, SymbLayer_ptr det_layer, node_ptr expr, node_ptr context, boolean in_next )
compileBEval.c
static node_ptr expr2bexpr_shift_left( BddEnc_ptr enc, SymbLayer_ptr det_layer, node_ptr context, boolean in_next, node_ptr a, node_ptr b, node_ptr def_case, int wb )
compileBEval.c
static node_ptr expr2bexpr_shift_right( BddEnc_ptr enc, SymbLayer_ptr det_layer, node_ptr context, boolean in_next, node_ptr a, node_ptr b, node_ptr def_case, int wb )
compileBEval.c
static node_ptr expr2bexpr_shift( BddEnc_ptr enc, SymbLayer_ptr det_layer, node_ptr expr, node_ptr context, boolean in_next )
compileBEval.c
static node_ptr expr2bexpr_word_ite_aux( BddEnc_ptr enc, SymbLayer_ptr det_layer, node_ptr expr, node_ptr context, boolean in_next )
compileBEval.c
static void flatten_declare_constants_within_list( node_ptr value_list, SymbLayer_ptr layer )
compileFlatten.c
static Set_t formulaGetDefinitionDependencies( const SymbTable_ptr symb_table, node_ptr formula, VarFilterType filter )
Formula_GetDependencies
compileCone.c
static Set_t formulaGetDependenciesRecur( const SymbTable_ptr symb_table, node_ptr formula, node_ptr context, VarFilterType filter )
formulaGetDefinitionDependencies
Formula_GetDependenciesByType
compileCone.c
static void init_check_program( node_ptr l )
compileCheck.c
static void make_params( node_ptr basename, node_ptr actual, node_ptr formal )
compileFlatten.c
static void print_assign( FILE * out, node_ptr lhs, node_ptr rhs )
compileWrite.c
static node_ptr put_in_context( node_ptr v )
param_context
.
param_context
compileFlatten.c
static node_ptr scalar_atom2bexpr( BddEnc_ptr enc, SymbLayer_ptr det_layer, node_ptr expr, node_ptr context, boolean in_next )
compileBEval.c
node_ptr sym_intern( char * s )
VAR x : {a1, a2, a3}; y : {a3, a4, a5}; ASSIGN next(x) := case x = y : a2; !(x = y) : a1; 1 : a3; esac;i.e. to allow the equality test between x and y. This can be performed because we internally have a unique representation of the atom a3.
find_atom
compileUtil.c
static const char* type_to_string( int type )
optional
compileFlatten.c
static int write_flatten_assign( const SymbTable_ptr symb_table, FILE* out, const NodeList_ptr vars, FlatHierarchy_ptr hierarchy )
compileWrite.c
static int write_flatten_define( const SymbTable_ptr symb_table, FILE* out, const NodeList_ptr names )
compileWrite.c
( )
Flatten_GetDefinition
compileFlatten.c
( )
compileFlatten.c
( )
compileCone.c
( )
compileCone.c
( )
compileCone.c
( )
compileUtil.c
( )
compile.h