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