1(IN-PACKAGE "ACL2")
2
3(INCLUDE-BOOK "sets")
4
5(DEFUN LTL-CONSTANTP (F)
6       (IF (EQUAL F 'TRUE)
7           (EQUAL F 'TRUE)
8           (EQUAL F 'FALSE)))
9
10(DEFUN LTL-VARIABLEP (F)
11       (IF (SYMBOLP F)
12           (NOT (MEMBERP F '(+ & U W X F G)))
13           'NIL))
14
15(DEFUN LTL-FORMULAP (F)
16       (IF (ATOM F)
17           (IF (LTL-CONSTANTP F)
18               (LTL-CONSTANTP F)
19               (LTL-VARIABLEP F))
20           (IF (EQUAL (LEN F) '3)
21               (IF (MEMBERP (CAR (CDR F)) '(+ & U W))
22                   (IF (LTL-FORMULAP (CAR F))
23                       (LTL-FORMULAP (CAR (CDR (CDR F))))
24                       'NIL)
25                   'NIL)
26               (IF (EQUAL (LEN F) '2)
27                   (IF (MEMBERP (CAR F) '(~ X F G))
28                       (LTL-FORMULAP (CAR (CDR F)))
29                       'NIL)
30                   'NIL))))
31
32(DEFUN RESTRICTED-FORMULAP (F V-LIST)
33       (IF (ATOM F)
34           (IF (LTL-CONSTANTP F)
35               (LTL-CONSTANTP F)
36               (IF (LTL-VARIABLEP F)
37                   (MEMBERP F V-LIST)
38                   'NIL))
39           (IF (EQUAL (LEN F) '3)
40               (IF (MEMBERP (CAR (CDR F)) '(& + U W))
41                   (IF (RESTRICTED-FORMULAP (CAR F) V-LIST)
42                       (RESTRICTED-FORMULAP (CAR (CDR (CDR F)))
43                                            V-LIST)
44                       'NIL)
45                   'NIL)
46               (IF (EQUAL (LEN F) '2)
47                   (IF (MEMBERP (CAR F) '(~ X F G))
48                       (RESTRICTED-FORMULAP (CAR (CDR F))
49                                            V-LIST)
50                       'NIL)
51                   'NIL))))
52
53(DEFTHM RESTRICTED-FORMULA-IS-AN-LTL-FORMULA
54        (IMPLIES (RESTRICTED-FORMULAP F V-LIST)
55                 (LTL-FORMULAP F)))
56
57(DEFUN CREATE-RESTRICTED-VAR-SET (F)
58       (IF (ATOM F)
59           (IF (LTL-CONSTANTP F)
60               'NIL
61               (CONS F 'NIL))
62           (IF (EQUAL (LEN F) '3)
63               (SET-UNION (CREATE-RESTRICTED-VAR-SET (CAR F))
64                          (CREATE-RESTRICTED-VAR-SET (CAR (CDR (CDR F)))))
65               (IF (EQUAL (LEN F) '2)
66                   (CREATE-RESTRICTED-VAR-SET (CAR (CDR F)))
67                   'NIL))))
68
69(DEFTHM LTL-FORMULA-IS-A-RESTRICTED-FORMULA
70        (IMPLIES (LTL-FORMULAP F)
71                 (RESTRICTED-FORMULAP F (CREATE-RESTRICTED-VAR-SET F))))
72
73(DEFUN NEXT-STATEP (P Q M) (MEMBERP Q (G P (G ':TRANSITION M))))
74
75(DEFUN INITIAL-STATEP (P M) (MEMBERP P (G ':INITIAL-STATES M)))
76
77(DEFUN LABEL-OF (S M) (G S (G ':LABEL-FN M)))
78
79(DEFUN NEXT-STATES-IN-STATES (M STATES)
80       (IF (ENDP STATES)
81           'T
82           (IF (SUBSET (G (CAR STATES) (G ':TRANSITION M))
83                       (G ':STATES M))
84               (NEXT-STATES-IN-STATES M (CDR STATES))
85               'NIL)))
86
87(DEFTHM NEXT-STATES-IN-STATES-CLARIFIED-AUX
88        (IMPLIES (IF (MEMBERP P STATES)
89                     (IF (NEXT-STATES-IN-STATES M STATES)
90                         (NEXT-STATEP P Q M)
91                         'NIL)
92                     'NIL)
93                 (MEMBERP Q (G ':STATES M))))
94
95(DEFTHM NEXT-STATES-IN-STATES-CLARIFIED
96        (IMPLIES (IF (NEXT-STATES-IN-STATES M (G ':STATES M))
97                     (IF (MEMBERP P (G ':STATES M))
98                         (NEXT-STATEP P Q M)
99                         'NIL)
100                     'NIL)
101                 (MEMBERP Q (G ':STATES M))))
102