smv-nt2[1].5工具软件2.5版

/***************************************************************************\ * * * Changed to implement bounded until - Sergio Campos - 05/92 * * * * Changed implementation of bounded for SMV 2.3 * * - steed@iil.intel.com - 07/92 * * * * Corrected implementation of bounded for SMV 2.4 * * - steed@iil.intel.com - 10/92 * * * * Implemented COMPUTE MIN and COMPUTE MAX properties * * - Sergio Campos, Will Marrero, Marius Minea - 05/94 * * * * Inserted the specification printing in check_AG_only (for -AG option)/ * * - Sergey Berezin - 03/98 * * * \***************************************************************************/ #include <stdio.h> #include "storage.h" #include "smvstring.h" #include "node.h" #include "hash.h" #include "bdd.h" #include "assoc.h" #include "y.tab.h" #include "lost.h" #include <stdlib.h> static hash_ptr module_hash; static hash_ptr symbol_hash; static hash_ptr param_hash; static hash_ptr constant_hash; static hash_ptr print_hash; static hash_ptr assign_hash; static hash_ptr global_assign_hash; static hash_ptr frame_hash; static hash_ptr value_hash; static hash_ptr state_hash; static int enforce_constant = 0; static node_ptr module_stack = NIL; node_ptr variables = NIL; static node_ptr all_symbols = NIL; static node_ptr heuristic_order = NIL; static bdd_ptr vars,input_vars; static int is_input_decl = 0; static int assign_type; static int instantiate_mode; static node_ptr the_impl; static node_ptr real_state_variables = NIL; int option_kripke = 1; #define NSTBASE 16 int nstvars = NSTBASE,real_nstvars=0,nstbase=NSTBASE; #define MAXSTVARS 500 #define EVALUATING ((bdd_ptr)(-1)) #define TYPE_ERROR ((node_ptr)(-1)) extern int verbose; extern int indent_size; extern int yylineno; extern node_ptr parse_tree; extern int option_incremental; #ifdef REORDER extern int reorder; #endif #ifdef OTHER_SIMP extern int option_othersimp; extern int option_early; extern int option_checktrans; extern int option_drip; extern int disable_reorder; static int check_AG_only(); #endif #ifdef SMV_SIGNALS extern int option_quit; #endif #ifdef OTHER_SIMP static node_ptr trans_expr,init_expr,spec_expr,fair_expr,assign_expr,procs; #endif static bdd_ptr eval(); static bdd_ptr trans=NULL; /* TRANS expr, ASSIGN next(v) := expr */ static bdd_ptr invar; /* ASSIGN v := expr (normal assignments) */ static bdd_ptr init; /* INIT expr, ASSIGN init(v) := expr */ static bdd_ptr frame; extern int option_conj_part,conj_part_limit; static node_ptr cp_trans=NIL,forward_quantifiers=NIL,reverse_quantifiers=NIL; static bdd_ptr reachable_states = (bdd_ptr)0; static node_ptr fairness_const = NIL; static bdd_ptr fair_states = (bdd_ptr)0; static bdd_ptr proc_selector; static bdd_ptr running; static node_ptr the_node; static node_ptr boolean_type; static node_ptr zero_number,one_number; static node_ptr running_atom; static bdd_ptr orig_trans,orig_init; static node_ptr orig_fairness_const; /* added by Hiromi to fix process_bug. 1998.5.5 */ static int checking_spec = 0; static bdd_ptr proc_sel_support; extern bdd_ptr forsome(),forall(),support_bdd(); node_ptr string_to_atom(s) char *s; { return(find_node(ATOM,find_string(s),NIL)); } node_ptr find_atom(a) node_ptr a; { if(a == NIL)return(a); return(find_node(a->type,a->left.nodetype,a->right.nodetype)); } static int eval_num(e,context) node_ptr e,context; { node_ptr n; bdd_ptr d; int temp = enforce_constant; enforce_constant = 1; d = eval(e,context); enforce_constant = temp; if(!ISLEAF(d))catastrophe("eval_num: !ISLEAF(d)"); n=(node_ptr)(d->left); if(n->type != NUMBER)rpterr("numeric constant required"); enforce_constant = temp; return(n->left.inttype); } bdd_ptr get_definition(n) node_ptr n; { node_ptr def = find_assoc(symbol_hash,n); bdd_ptr res; if(!def)return((bdd_ptr)0); if(enforce_constant && def->type == VAR)rpterr("constant required"); if(def->type == BDD || def->type == VAR) return(save_bdd((bdd_ptr)car(def))); res = (bdd_ptr)find_assoc(value_hash,n); if(res == EVALUATING)circular(n); if(res)return(save_bdd(res)); if(verbose > 1){ indent_size++; indent_node(stderr,"evaluating ",n,":\n"); } insert_assoc(value_hash,n,EVALUATING); push_atom(n); res = eval(def,NIL); pop_atom(n); insert_assoc(value_hash,n,save_bdd(res)); if(verbose > 1){ indent_node(stderr,"size of ",n," = "); fprintf(stderr,"%d BDD nodes\n",size_bdd(res)); indent_size--; } return(res); } static bdd_ptr eval_sign(a,flag) bdd_ptr a; int flag; { switch(flag){ case -1: return(not_bdd(a)); default: return(a); } } static bdd_ptr unary_op(op,n,resflag,argflag,context) bdd_ptr (*op)(); node_ptr n,context; int resflag,argflag; { bdd_ptr arg = eval(car(n),context); release_bdd(arg); the_node = n; return(save_bdd(eval_sign(op(eval_sign(arg,argflag)),resflag))); } static bdd_ptr binary_op(op,n,resflag,argflag1,argflag2,context) bdd_ptr (*op)(); node_ptr n,context; int resflag,argflag1,argflag2; { bdd_ptr arg1 = eval(car(n),context); bdd_ptr arg2 = eval(cdr(n),context); release_bdd(arg1); release_bdd(arg2); the_node = n; return(save_bdd(eval_sign(op(eval_sign(arg1,argflag1), eval_sign(arg2,argflag2)), resflag))); } #ifdef TIMING static bdd_ptr binary_op1(op,n,resflag,argflag1,argflag2,context) bdd_ptr (*op)(); node_ptr n,context; int resflag,argflag1,argflag2; { bdd_ptr arg1 = eval(car(n),context); bdd_ptr arg2 = eval(cdr(n),context); release_bdd(arg1); release_bdd(arg2); the_node = n; return(op(eval_sign(arg1,argflag1), eval_sign(arg2,argflag2))); } #endif static bdd_ptr ternary_op(op,n,resflag,argflag,context) bdd_ptr (*op)(); node_ptr n,context; int resflag,argflag; { bdd_ptr arg1 = eval(car(n),context); int arg2 = eval_num(car(cdr(n)),context); int arg3 = eval_num(cdr(cdr(n)),context); release_bdd(arg1); the_node = n; return(save_bdd(eval_sign(op(eval_sign(arg1,argflag), arg2, arg3), resflag))); } static bdd_ptr quad_op(op, n, resflag, argflag1, argflag2, context) bdd_ptr (*op)(); node_ptr n,context; int resflag,argflag1,argflag2; { bdd_ptr arg1 = eval(car(car(n)), context); bdd_ptr arg2 = eval(cdr(car(n)), context); int arg3 = eval_num(car(cdr(n)), context); int arg4 = eval_num(cdr(cdr(n)), context); release_bdd(arg1); release_bdd(arg2); the_node = n; return(save_bdd(eval_sign(op(eval_sign(arg1,argflag1), eval_sign(arg2,argflag2), arg3, arg4), resflag))); } static bdd_ptr eval_if_then_else(ifexp,thenexp,elseexp,context) node_ptr ifexp,thenexp,elseexp,context; { bdd_ptr ifarg = eval(ifexp,context); bdd_ptr thenarg = eval(thenexp,context); bdd_ptr elsearg = eval(elseexp,context); release_bdd(ifarg); release_bdd(thenarg); release_bdd(elsearg); return(save_bdd(if_then_else_bdd(ifarg,thenarg,elsearg))); } static node_ptr eval_struct(); static node_ptr eval_struct1(n,context) node_ptr n,context; { node_ptr temp,name; switch(n->type){ case CONTEXT: return(eval_struct(cdr(n),car(n))); case ATOM: name = find_node(DOT,context,find_atom(n)); if(temp = find_assoc(param_hash,name)) return(eval_struct(temp,context)); return(name); case DOT: temp = eval_struct(car(n),context