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