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 )
int Compile_CheckWff( node_ptr wff, node_ptr context )
check_wff_recur
void Compile_End( )
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 * 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
node_ptr Compile_FlattenSexpExpandDefine( const Encoding_ptr senc, node_ptr sexp, node_ptr context )
Flatten_GetDefinition
node_ptr Compile_FlattenSexp( const Encoding_ptr senc, node_ptr sexp, node_ptr context )
Flatten_GetDefinition
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 * 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
void Compile_InitializeBuildModel( )
optional
void Compile_Init( )
int Compile_WriteFlattenBool( const Encoding_ptr senc, FILE* out, SexpFsm_ptr fsm, cmp_struct_ptr s )
int Compile_WriteFlatten( const Encoding_ptr senc, FILE* out, cmp_struct_ptr s )
NodeList_ptr Compile_get_expression_dependencies( const Encoding_ptr senc, Expr_ptr expression )
boolean Compile_is_input_variable_formula( const Encoding_ptr senc, node_ptr n )
void compile_create_flat_model( )
Expr_ptr compile_flatten_resolve_name_recur( Expr_ptr n, node_ptr context )
CompileFlatten_resolve_name
.
CompileFlatten_resolve_name