1 2(*****************************************************************************) 3(* Data.sml -- the abstract syntax datatype for PSL/Sugar *) 4(*****************************************************************************) 5 6 7(****************************************************************************** 8* Boolean expressions 9******************************************************************************) 10datatype bexp = 11 B_PROP of string (* atomic proposition *) 12 | B_NOT of bexp (* negation *) 13 | B_AND of bexp * bexp (* conjunction *) 14(*========= Following are defined operators (i.e. syntactic sugar) =========*) 15 | B_OR of bexp * bexp (* disjunction *) 16 | B_IMP of bexp * bexp (* implication *) 17 | B_IFF of bexp * bexp (* logical equivalence *) 18 | B_TRUE (* T *) 19 | B_FALSE (* F *) 20; 21 22(****************************************************************************** 23* Specification of an iteration number or range (Count of LRM A.3.6) 24******************************************************************************) 25type range = int * int option; 26 27(****************************************************************************** 28* Sequential Extended Regular Expressions (SEREs) 29******************************************************************************) 30datatype sere = 31 S_BOOL of bexp (* boolean expression *) 32 | S_CAT of sere * sere (* r1 ; r2 *) 33 | S_FUSION of sere * sere (* r1 : r2 *) 34 | S_OR of sere * sere (* r1 | r2 *) 35 | S_AND of sere * sere (* r1 && r2 *) 36 | S_REPEAT of sere (* r[*] *) 37 | S_CLOCK of sere * bexp (* r@clk *) 38(*========= Following are defined operators (i.e. syntactic sugar) =========*) 39 | S_FLEX_AND of sere * sere (* r1 & r2 *) 40 | S_RANGE_REPEAT of sere * range (* r[* i] *) 41 | S_NON_ZERO_REPEAT of sere (* r[+] *) 42 | S_RANGE_EQ_REPEAT of bexp * range (* r[= i] *) 43 | S_RANGE_GOTO_REPEAT of bexp * range (* r[-> i] *) 44; 45 46(****************************************************************************** 47* Formulas of the Foundation Language (FL) 48******************************************************************************) 49datatype fl = 50 F_BOOL of bexp (* boolean expression *) 51 | F_NOT of fl (* \neg f *) 52 | F_AND of fl * fl (* f1 \wedge f2 *) 53 | F_STRONG_X of fl (* X! f *) 54 | F_U of fl * fl (* [f1 U f2] *) 55 | F_SUFFIX_IMP of sere * fl (* {r}(f) *) 56 | F_STRONG_IMP of sere * sere (* {r1} |-> {r2}! *) 57 | F_WEAK_IMP of sere * sere (* {r1} |-> {r2} *) 58 | F_ABORT of fl * bexp (* f abort b *) 59 | F_STRONG_CLOCK of fl * bexp (* f@clk! *) 60(*========= Following are defined operators (i.e. syntactic sugar) =========*) 61 | F_WEAK_CLOCK of fl * bexp (* f@clk *) 62 | F_OR of fl * fl (* f1 \vee f2 *) 63 | F_IMP of fl * fl (* f1 \rightarrow f2 *) 64 | F_IFF of fl * fl (* f1 \leftrightarrow f2 *) 65 | F_WEAK_X of fl (* X f *) 66 | F_F of fl (* F f *) 67 | F_G of fl (* G f *) 68 | F_W of fl * fl (* [f1 W f2] *) 69 | F_ALWAYS of fl (* always f *) 70 | F_NEVER of fl (* never f *) 71 | F_WEAK_NEXT of fl (* next f *) 72 | F_STRONG_NEXT of fl (* next! f *) 73 | F_STRONG_EVENTUALLY of fl (* next! f *) 74 | F_STRONG_UNTIL of fl * fl (* [f1 until! f2] *) 75 | F_WEAK_UNTIL of fl * fl (* [f1 until f2] *) 76 | F_STRONG_UNTIL_INC of fl * fl (* [f1 until!_ f2] *) 77 | F_WEAK_UNTIL_INC of fl * fl (* [f1 until_ f2] *) 78 | F_STRONG_BEFORE of fl * fl (* [f1 before! f2] *) 79 | F_WEAK_BEFORE of fl * fl (* [f1 before f2] *) 80 | F_STRONG_BEFORE_INC of fl * fl (* [f1 before!_ f2] *) 81 | F_WEAK_BEFORE_INC of fl * fl (* [f1 before_ f2] *) 82 | F_NUM_WEAK_X of int * fl (* X[n](f) *) 83 | F_NUM_STRONG_X of int * fl (* X *) 84 | F_NUM_WEAK_NEXT of int * fl (* next[n](f) *) 85 | F_NUM_STRONG_NEXT of int * fl (* next *) 86 | F_NUM_WEAK_NEXT_A of range * fl (* next_a[n](f) *) 87 | F_NUM_STRONG_NEXT_A of range * fl (* next_a *) 88 | F_NUM_WEAK_NEXT_E of range * fl (* next_e[n](f) *) 89 | F_NUM_STRONG_NEXT_E of range * fl (* next_e *) 90 | F_STRONG_NEXT_EVENT of bexp * fl (* next_event!(b)(f) *) 91 | F_WEAK_NEXT_EVENT of bexp * fl (* next_event(b)(f) *) 92 | F_NUM_STRONG_NEXT_EVENT 93 of bexp * int * fl (* next_event!(b)[i](f) *) 94 | F_NUM_WEAK_NEXT_EVENT 95 of bexp * int * fl (* next_event(b)[i](f) *) 96 | F_NUM_STRONG_NEXT_EVENT_A 97 of bexp * range * fl (* next_event_a!(b)[i](f) *) 98 | F_NUM_WEAK_NEXT_EVENT_A 99 of bexp * range * fl (* next_event_a(b)[i](f) *) 100 | F_NUM_STRONG_NEXT_EVENT_E 101 of bexp * range * fl (* next_event_e!(b)[i](f) *) 102 | F_NUM_WEAK_NEXT_EVENT_E 103 of bexp * range * fl (* next_event_e(b)[i](f) *) 104 | F_SKIP_STRONG_IMP of sere * sere (* {r1} |=> {r2}! *) 105 | F_SKIP_WEAK_IMP of sere * sere (* {r1} |=> {r2} *) 106 | F_SERE_ALWAYS of sere (* always r *) 107 | F_SERE_NEVER of sere (* never r *) 108 | F_SERE_STRONG_EVENTUALLY 109 of sere (* eventually! r *) 110 | F_STRONG_WITHIN of sere * bexp * sere (* within!(r1,b)r2 *) 111 | F_WEAK_WITHIN of sere * bexp * sere (* within(r1,b)r2 *) 112 | F_STRONG_WITHIN_INC of sere * bexp * sere (* within!_(r1,b)r2 *) 113 | F_WEAK_WITHIN_INC of sere * bexp * sere (* within_(r1,b)r2 *) 114 | F_STRONG_WHILENOT of bexp * sere (* whilenot!(b)r *) 115 | F_WEAK_WHILENOT of bexp * sere (* whilenot(b)r *) 116 | F_STRONG_WHILENOT_INC 117 of bexp * sere (* whilenot!_(b)r *) 118 | F_WEAK_WHILENOT_INC of bexp * sere (* whilenot_(b)r *) 119; 120 121 122(****************************************************************************** 123* Formulas of the Optional Branching Extension (OBE) 124******************************************************************************) 125datatype obe = 126 O_BOOL of bexp (* boolean expression *) 127 | O_NOT of obe (* \neg f *) 128 | O_AND of obe * obe (* f1 \wedge f2 *) 129 | O_EX of obe (* EX f *) 130 | O_EU of obe * obe (* E[f1 U f2] *) 131 | O_EG of obe (* EG f *) 132; 133 134 135