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