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 CommandCheckWff( 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 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_quit_flattener( )
compileFlatten.c
Expr_ptr CompileFlatten_resolve_name( Expr_ptr expr, 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.
compile_flatten_resolve_name_recur
compileFlatten.c
void Compile_CheckProgram( node_ptr procs, node_ptr spec_expr, node_ptr ltlspec_expr, node_ptr invar_expr, node_ptr justice_expr, node_ptr compassion_expr )
compileCheck.c
int Compile_CheckWff( node_ptr wff, node_ptr context )
check_wff_recur
compileCheckWff.c
void Compile_End( )
compileCmd.c
void
Compile_FlattenHierarchy(
Encoding_ptr senc,
node_ptr root_name, the ATOM
representing the module at
the top of the hierarchy.
node_ptr name, the name of the module at the top of the hierarchy.
node_ptr * trans, the list of TRANS actually recognized
node_ptr * init, the list of INIT actually recognized
node_ptr * invar, the list of INVAR actually recognized
node_ptr * spec, the list of SPEC actually recognized
node_ptr * compute, the list of COMPUTE actually recognized
node_ptr * ltl_spec, the list of LTLSPEC actually recognized
node_ptr * psl_spec, the list of PSLSPEC actually recognized
node_ptr * invar_spec, the list of INVARSPEC actually recognized
node_ptr * justice, the list of JUSTICE actually recognized
node_ptr * compassion, the list of COMPASSION actually recognized
node_ptr * procs, the list of processes actually recognized
node_ptr actual the actual module arguments
)
compileFlattenHierarchy
compileFlatten.c
node_ptr Compile_FlattenSexpExpandDefine( const Encoding_ptr senc, node_ptr sexp, node_ptr context )
Flatten_GetDefinition
compileFlatten.c
node_ptr Compile_FlattenSexp( const Encoding_ptr senc, node_ptr sexp, node_ptr context )
Flatten_GetDefinition
compileFlatten.c
void
Compile_FlattenTableau(
Encoding_ptr senc,
node_ptr root_name, the ATOM
representing the module at the top of the hierarchy.
node_ptr name, the name of the module at the top of the hierarchy.
node_ptr * trans, the list of TRANS actually recognized
node_ptr * init, the list of INIT actually recognized
node_ptr * invar, the list of INVAR actually recognized
node_ptr * spec, the list of SPEC actually recognized
node_ptr * compute, the list of COMPUTE actually recognized
node_ptr * ltl_spec, the list of LTLSPEC actually recognized
node_ptr * psl_spec, the list of PSLSPEC actually recognized
node_ptr * invar_spec, the list of INVARSPEC actually recognized
node_ptr * justice, the list of JUSTICE actually recognized
node_ptr * compassion, the list of COMPASSION actually recognized
node_ptr * procs, the list of processes actually recognized
node_ptr actual the actual module arguments
)
Compile_FlattenHierarchy
compileFlattenHierarchy
compileFlatten.c
void Compile_InitializeBuildModel( )
optional
compileUtil.c
void Compile_Init( )
compileCmd.c
int Compile_WriteFlattenBool( const Encoding_ptr senc, FILE* out, SexpFsm_ptr fsm, cmp_struct_ptr s )
compileWriteBool.c
int Compile_WriteFlatten( const Encoding_ptr senc, FILE* out, cmp_struct_ptr s )
compileWriteFlat.c
NodeList_ptr Compile_get_expression_dependencies( const Encoding_ptr senc, Expr_ptr expression )
compileCheck.c
boolean Compile_is_input_variable_formula( const Encoding_ptr senc, node_ptr n )
compileCheckWff.c
Set_t ComputeCOI( const Encoding_ptr senc, Set_t base )
compileCone.c
static node_ptr Flatten_FlattenSexpRecur( const Encoding_ptr senc, node_ptr sexp, node_ptr context )
Compile_FlattenSexp
Compile_FlattenSexpExpandDefine
compileFlatten.c
node_ptr Flatten_GetDefinition( const Encoding_ptr senc, node_ptr atom )
compileFlatten.c
Set_t Formula_GetDependencies( const Encoding_ptr senc, node_ptr formula, node_ptr context )
formulaGetDefinitionDependencies
compileCone.c
Set_t Formulae_GetDependencies( const Encoding_ptr senc, node_ptr formula, node_ptr justice, node_ptr compassion )
compileCone.c
BddFsm_ptr FsmBuilder_create_bdd_fsm( const FsmBuilder_ptr self, BddEnc_ptr enc, const SexpFsm_ptr sexp_fsm, const TransType trans_type )
compileFsmMgr.c
SexpFsm_ptr FsmBuilder_create_sexp_fsm( const FsmBuilder_ptr self, const Encoding_ptr senc, VarSet_ptr vars_list, const enum SexpFsmType type )
compileFsmMgr.c
FsmBuilder_ptr FsmBuilder_create( DdManager* dd )
compileFsmMgr.c
void FsmBuilder_destroy( FsmBuilder_ptr self )
compileFsmMgr.c
static node_ptr add2bexpr_recur( BddEnc_ptr enc, add_ptr bool_add, boolean in_next, boolean allow_nondet, hash_ptr lc )
add2bexpr
Utils_is_in_range
compileBEval.c
static node_ptr add2bexpr( add_ptr bool_add, boolean in_next, boolean allow_nondet )
add2bexpr_recur
mk_new_var
compileBEval.c
static void check_assign_both( node_ptr v, int node_type, int lineno )
compileCheck.c
static void check_assign( BddEnc_ptr enc, node_ptr n, node_ptr context, int mode )
compileCheck.c
static void check_circular_assign( BddEnc_ptr enc, node_ptr n, node_ptr context, boolean is_next, boolean is_lhs, boolean lhs_is_next )
compileCheck.c
static void check_circ( BddEnc_ptr enc, 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
static wff_result_type check_definition( BddEnc_ptr enc, node_ptr n )
n
, this
function returns the its definition as a wff result.
Compile_CheckWff
compileCheckWff.c
static wff_result_type check_wff_recur( BddEnc_ptr enc, node_ptr wff, node_ptr context )
Compile_CheckWff
function.
Compile_CheckWff
compileCheckWff.c
void check_wff( node_ptr wff, node_ptr context )
Compile_CheckWff
check_wff_recur
compileCheckWff.c
static void coiInit( const Encoding_ptr senc )
ComputeCOI
compileCone.c
void compileCheckAssignForInputVars( Encoding_ptr senc, node_ptr assign )
compileCheck.c
void compileCheckForInputVars( Encoding_ptr senc, node_ptr trans_expr, node_ptr init_expr, node_ptr invar_expr, node_ptr assign_expr )
compileCheck.c
void compileCheckInitForInputVars( Encoding_ptr senc, node_ptr init )
compileCheck.c
void compileCheckInvarForInputVars( Encoding_ptr senc, node_ptr invar )
compileCheck.c
void compileCheckTransForInputVars( Encoding_ptr senc, node_ptr trans )
compileCheck.c
boolean compileExpressionHasNextInputs( Encoding_ptr senc, node_ptr expr )
compileCheck.c
static Set_t compileFlattenConstantSexpCheck( Encoding_ptr senc, node_ptr expr, int type )
optional
compileFlatten.c
static void
compileFlattenHierarchy(
Encoding_ptr senc,
node_ptr root_name, the ATOM
representing the module
at the top of the hierarchy.
node_ptr name, the name of the module at the top of the hierarchy.
node_ptr * trans, the list of TRANS actually recognized
node_ptr * init, the list of INIT actually recognized
node_ptr * invar, the list of INVAR actually recognized
node_ptr * spec, the list of SPEC actually recognized
node_ptr * compute, the list of COMPUTE actually recognized
node_ptr * ltl_spec, the list of LTLSPEC actually recognized
node_ptr * psl_spec, the list of PSLSPEC actually recognized
node_ptr * invar_spec, the list of INVARSPEC actually recognized
node_ptr * justice, the list of JUSTICE actually recognized
node_ptr * compassion, the list of COMPASSION actually recognized
node_ptr * assign, the list of ASSIGN actually recognized
node_ptr * procs, the list of processes actually recognized
node_ptr actual the actual module arguments
)
compileFlatten.c
static void compileFlattenProcessRecur( const Encoding_ptr senc, node_ptr assign, node_ptr context, node_ptr running )
compileFlatten.c
node_ptr compileFlattenProcess( Encoding_ptr senc, node_ptr procs_expr )
compileFlatten.c
static void compileFlattenSexpModelAux( Encoding_ptr senc, node_ptr expr, int type )
optional
compileFlatten.c
static void compileFlattenSexpModelRecur( Encoding_ptr senc, node_ptr expr, int type )
optional
compileFlatten.c
void compileFlattenSexpModel( Encoding_ptr senc, node_ptr init_expr, node_ptr invar_expr, node_ptr trans_expr )
Compile_FlattenProcess
compileFlatten.c
void compile_create_flat_model( )
compileCmd.c
Expr_ptr compile_flatten_resolve_name_recur( Expr_ptr n, node_ptr context )
CompileFlatten_resolve_name
.
CompileFlatten_resolve_name
compileFlatten.c
int compile_write_flatten_psl( const Encoding_ptr senc, FILE* out, node_ptr n )
compileWriteBool.c
int compile_write_flatten_psl( const Encoding_ptr senc, FILE* out, node_ptr n )
compileWriteFlat.c
static void create_process_symbolic_variables( Encoding_ptr senc, node_ptr procs_expr )
compileFlatten.c
Expr_ptr detexpr2bexpr( Expr_ptr expr )
expr2bexpr
expr2bexpr_recur
compileBEval.c
static node_ptr expr2bexpr_recur( BddEnc_ptr enc, node_ptr expr, boolean in_next, boolean allow_nondet )
expr2bexpr
detexpr2bexpr
compileBEval.c
Expr_ptr expr2bexpr( Expr_ptr expr )
detexpr2bexpr
expr2bexpr_recur
compileBEval.c
static Set_t formulaGetDefinitionDependencies( const Encoding_ptr senc, node_ptr formula )
Formula_GetDependencies
compileCone.c
static Set_t formulaGetDependenciesRecur( const Encoding_ptr senc, node_ptr formula, node_ptr context )
Formula_GetDependencies
formulaGetDefinitionDependencies
compileCone.c
static void fsm_builder_clusterize_expr_aux( const FsmBuilder_ptr self, BddEnc_ptr enc, ClusterList_ptr clusters, Expr_ptr expr_trans, boolean is_inside_and )
compileFsmMgr.c
static ClusterList_ptr fsm_builder_clusterize_expr( FsmBuilder_ptr self, BddEnc_ptr enc, Expr_ptr expr )
compileFsmMgr.c
static CompassionList_ptr fsm_builder_compassion_sexp_to_bdd( FsmBuilder_ptr self, BddEnc_ptr enc, node_ptr compassion_sexp_list )
compileFsmMgr.c
static void fsm_builder_deinit( FsmBuilder_ptr self )
compileFsmMgr.c
static void fsm_builder_init( FsmBuilder_ptr self, DdManager* dd )
compileFsmMgr.c
static JusticeList_ptr fsm_builder_justice_sexp_to_bdd( FsmBuilder_ptr self, BddEnc_ptr enc, node_ptr justice_sexp_list )
compileFsmMgr.c
static void init_check_program_recur( node_ptr l )
compileCheck.c
static void init_check_program( node_ptr procs_exp )
compileCheck.c
static void instantiate_by_name( Encoding_ptr senc, node_ptr root_name, node_ptr name, node_ptr * trans, node_ptr * init, node_ptr * invar, node_ptr * spec, node_ptr * compute, node_ptr * ltl_spec, node_ptr * psl_spec, node_ptr * invar_spec, node_ptr * justice, node_ptr * compassion, node_ptr * assign, node_ptr * procs, node_ptr actual )
compileFlatten.c
void instantiate_vars( Encoding_ptr senc, node_ptr var_list, node_ptr mod_name, node_ptr * trans, node_ptr * init, node_ptr * invar, node_ptr * spec, node_ptr * compute, node_ptr * ltl_spec, node_ptr * psl_spec, node_ptr * invar_spec, node_ptr * justice, node_ptr * compassion, node_ptr * assign, node_ptr * procs )
instantiate_var
compileFlatten.c
void instantiate_var( Encoding_ptr senc, node_ptr name, node_ptr type, node_ptr * trans, node_ptr * init, node_ptr * invar, node_ptr * spec, node_ptr * compute, node_ptr * ltl_spec, node_ptr * psl_spec, node_ptr * invar_spec, node_ptr * justice, node_ptr * compassion, node_ptr * assign, node_ptr * procs, node_ptr context )
symbol_hash
saying that the variable range is {0,1}
.M..N
, then
we add an entry in the symbol_hash
saying that the
variable range is {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 range is
{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).
instantiate_vars
compileFlatten.c
static void instantiate( Encoding_ptr senc, node_ptr mod_def, node_ptr mod_name, node_ptr * trans, node_ptr * init, node_ptr * invar, node_ptr * spec, node_ptr * compute, node_ptr * ltl_spec, node_ptr * psl_spec, node_ptr * invar_spec, node_ptr * justice, node_ptr * compassion, node_ptr * assign, node_ptr * procs, node_ptr actual )
instantiate_var
instantiate_vars
compileFlatten.c
static node_ptr make_atom_set( node_ptr l )
compileFlatten.c
static void make_params( node_ptr basename, node_ptr actual, node_ptr formal )
compileFlatten.c
static node_ptr mk_and( node_ptr a, node_ptr b )
optional
compileFlatten.c
static node_ptr mk_false( )
optional
compileFlatten.c
static node_ptr mk_new_var( Encoding_ptr senc )
INT_VAR_PREFIX
det_counter
Compile_EncodeVar
compileBEval.c
static node_ptr mk_true( )
optional
compileFlatten.c
int parsecheckwffcmd( int argc, char ** argv, node_ptr * pc )
0
if an expected expression
has been parsed, 1
otherwise. The parsed expression is
stored in pc
.
compileCheckWff.c
static void print_assign( FILE * out, node_ptr lhs, node_ptr rhs )
compileWriteFlat.c
static void print_io_atom_stack_assign( FILE * fd )
compileCheck.c
static node_ptr put_in_context( node_ptr v )
param_context
.
param_context
compileFlatten.c
static node_ptr scalar_atom2bexpr( BddEnc_ptr enc, node_ptr expr, boolean in_next, boolean allow_nondet )
add2bexpr_recur
mk_new_var
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 char * type_to_string( int type )
optional
compileFlatten.c
static boolean wff_is_boolean( node_ptr l )
wff_is_numeric
compileCheckWff.c
static boolean wff_is_numeric( node_ptr l )
wff_is_boolean
compileCheckWff.c
static int write_flatten_assign( const Encoding_ptr senc, FILE* out )
write_flatten_assign_recur
compileWriteFlat.c
static int write_flatten_bfexpr( const Encoding_ptr senc, FILE* out, node_ptr n, char* s )
compileWriteBool.c
static int write_flatten_define( const Encoding_ptr senc, FILE* out )
compileWriteFlat.c
static int write_flatten_expr_pair( const Encoding_ptr senc, FILE* out, node_ptr l, char* s )
compileWriteBool.c
static int write_flatten_expr_pair( const Encoding_ptr senc, FILE* out, node_ptr l, char* s )
compileWriteFlat.c
static int write_flatten_expr( const Encoding_ptr senc, FILE* out, node_ptr n, char* s )
compileWriteBool.c
static int write_flatten_expr( const Encoding_ptr senc, FILE* out, node_ptr n, char* s )
compileWriteFlat.c
static int write_flatten_vars( const Encoding_ptr senc, FILE* out, node_ptr lov, char* str )
compileWriteBool.c
static int write_flatten_vars( const Encoding_ptr senc, FILE* out, node_ptr lov, char* str )
compileWriteFlat.c
static int write_process_selector_define( const Encoding_ptr senc, FILE* out )
compileWriteFlat.c
( )
Flatten_GetDefinition
compileFlatten.c
( )
compileCone.c
( )
compileCone.c
( )
compile.h