1signature translationsLib =
2sig
3
4  (******************************************************************
5   *
6   * ltl2omega_rewrite t ltl
7   * translates the ltl term ltl into an omega automaton and
8   * returns a theorem that states the equivalence of the automaton
9   * and the ltl formula. The parameter t is used to determine the kind
10   * of omega automaton. For t = TRUE an existential automaton
11   * otherwise an universal automaton is used.
12   *
13   * It uses only rewrite rules for this translation.
14   * Notice, that this is just a proof of concept. In practice
15   * ltl2omega should be used, since it is much more efficient.
16   *
17   *******************************************************************)
18  val ltl2omega_rewrite : bool -> Abbrev.term -> Abbrev.thm
19
20  (******************************************************************
21   *
22   * ltl2omega fast fast t ltl
23   * This function does the same translation as ltl2omega_rewrite.
24   * However, the implementation is more advanced. The parameter fast
25   * tells the function whether to search for multiple occurences of
26   * terms in the ltl formula. This may reduce the number of needed
27   * states of the resulting automaton. However, it slows down the
28   * translation in general.
29   *
30   *******************************************************************)
31  val ltl2omega : bool -> bool -> Abbrev.term -> Abbrev.thm
32
33
34  (******************************************************************
35   * ltl2omega_interal fast fast t ltl
36   * This function is similar to ltl2omega.
37   * It in fact forms the main part of the translation done by ltl2omega.
38   * In contrast to ltl2omega, it returns some internal data, that contain
39   * more informations than the theorem returned by ltl2omega.
40   * This function is used to implement rltl2fctl and ltl2fctl
41   *******************************************************************)
42  val ltl2omega_internal : bool -> bool -> bool -> Abbrev.term -> (Abbrev.term * Abbrev.thm * Abbrev.thm * Abbrev.term * Abbrev.term * bool * bool)
43
44
45  (********************************************************************
46   * These functions translate some ltl problems to an check whether there is
47   * an fair path through a kripke structure. This problem can be handeled by
48   * a model checker. The first parameter is always the knows fast switch
49   ********************************************************************)
50
51  val ltl_ks_sem2ks_fair_emptyness___no_ks : bool -> Abbrev.term -> Abbrev.thm
52  val ltl_ks_sem2ks_fair_emptyness : bool -> Abbrev.term -> Abbrev.term -> Abbrev.thm
53
54  val ltl_contradiction2ks_fair_emptyness : bool -> Abbrev.term -> Abbrev.thm
55  val ltl_equivalent2ks_fair_emptyness : bool -> Abbrev.term -> Abbrev.term -> Abbrev.thm
56  val ltl_equivalent_initial2ks_fair_emptyness : bool -> Abbrev.term -> Abbrev.term -> Abbrev.thm
57
58
59
60  (********************************************************************
61   * These functions translate some ltl problems to an check whether there is
62   * an fair path through a kripke structure. Thereby they replace all variables
63   * by natural numbers, such that a lot of ugly precondition like INJ or
64   * ITERATORS are not necessary any more. There are different modes for this
65   * functions. mode 1 generates an implication theorem. mode 2 an equational
66   * theorem and all other mode both therorem. Additionally these functions
67   * return a list, that tells which numbers represent the original varibales
68   ********************************************************************)
69  val ltl_contradiction2ks_fair_emptyness___num: int -> bool -> Abbrev.term -> (Abbrev.thm * ((int * Abbrev.term) list))
70  val ltl_equivalent2ks_fair_emptyness___num: int -> bool -> Abbrev.term -> Abbrev.term -> (Abbrev.thm * ((int * Abbrev.term) list))
71  val ltl_equivalent_initial2ks_fair_emptyness___num: int -> bool -> Abbrev.term -> Abbrev.term -> (Abbrev.thm * ((int * Abbrev.term) list))
72
73  val ltl_ks_sem2ks_fair_emptyness___num : int -> bool -> Abbrev.term -> Abbrev.term -> (Abbrev.thm * ((int * Abbrev.term) list))
74
75
76
77
78  (********************************************************************
79   * Similar functions for PSL, that internally use the LTL versions
80   ********************************************************************)
81
82
83  val psl_ks_sem2ks_fair_emptyness___no_ks : bool -> Abbrev.term -> Abbrev.thm
84  val psl_ks_sem2ks_fair_emptyness : bool -> Abbrev.term -> Abbrev.term -> Abbrev.thm
85
86  val psl_contradiction2ks_fair_emptyness : bool -> Abbrev.term -> Abbrev.thm
87  val psl_equivalent2ks_fair_emptyness : bool -> Abbrev.term -> Abbrev.term -> Abbrev.thm
88
89  val psl_contradiction2ks_fair_emptyness___num: int -> bool -> Abbrev.term -> (Abbrev.thm * ((int * Abbrev.term) list))
90  val psl_equivalent2ks_fair_emptyness___num: int -> bool -> Abbrev.term -> Abbrev.term -> (Abbrev.thm * ((int * Abbrev.term) list))
91
92  val psl_ks_sem2ks_fair_emptyness___num : int -> bool -> Abbrev.term -> Abbrev.term -> (Abbrev.thm * ((int * Abbrev.term) list))
93end
94
95