1signature modelCheckLib = 2sig 3 4(*These lib is an interface to modelcheckers. The translationLib is 5 used to translate several model checking problems to a check for the 6 existance of a fair path through a kripke structure. Then a model checker 7 is used to check these properties. At the moment SMV and temporalLib by 8 Klaus Schneider are used. Thus, temporalLib has to work correctly, to 9 make these lib work. Thus maker sure, the parameter smv_path of temporalLib 10 has been ajusted to your systems and the examples for temporalLib work, 11 before trying to use this lib. 12 13 14 All functions return a thm option. If the specific property can be 15 proved they return a theorem thm stating the property in the form 16 SOME thm. If it can not be proved these functions print out a 17 path showing a counterexample and return NONE. 18*) 19 20(*The file used to interact with smv*) 21val model_check_temp_file : string ref; 22 23val ctl_ks_fair2smv_string : Abbrev.term -> TextIO.outstream -> string 24val fair_empty_ks2smv_string : Abbrev.term -> TextIO.outstream -> string 25 26val model_check___ks_fair_emptyness : Abbrev.thm -> Abbrev.thm option 27val modelCheckFairEmptyness : Abbrev.term -> Abbrev.thm -> bool 28 29 30(*Checks that the given ltl-formula is a contradiction, i.e. that there 31 is no path satisfing the formula*) 32val model_check___ltl_contradiction : Abbrev.term -> Abbrev.thm option 33 34 35(*Checks that the given ltl-formulas are equivalent at the first point of time. Since there are past ltl operators this does not mean that they are equivalent for all points of time!*) 36val model_check___ltl_equivalent_initial : Abbrev.term -> Abbrev.term -> Abbrev.thm option 37 38(*Checks that the given ltl-formulas are equivalent at all points of time.*) 39val model_check___ltl_equivalent : Abbrev.term -> Abbrev.term -> Abbrev.thm option 40 41(*model_check___ltl_ks_sem f M 42checks that the given kripke_structure M models the ltl-formula f. 43M has to be given in the form 44 45symbolic_kripke_structure S0 R 46 47where S0 and R may only contain, negations, conjunctions, disjuctions, implications and equivalences als boolean operators.*) 48val model_check___ltl_ks_sem : Abbrev.term -> Abbrev.term -> Abbrev.thm option 49 50 51(*Checks that the given sere and clock free PSL formula is a contradiction 52 on infinite TOP and BOTTOM free paths, i.e. there is no 53 infinite path that contains only "normal" states that fulfils the 54 formula*) 55val model_check___psl_contradiction : Abbrev.term -> Abbrev.thm option 56 57(*Checks that the given sere and clock free PSL formulas are equivalent 58 on infinite TOP and BOTTOM free paths*) 59val model_check___psl_equivalent : Abbrev.term -> Abbrev.term -> Abbrev.thm option 60 61(*Checks that the given sere and clock free PSL formulas is modeled by 62 a kripke_structure.*) 63val model_check___psl_ks_sem : Abbrev.term -> Abbrev.term -> Abbrev.thm option 64 65end 66 67