-
Notifications
You must be signed in to change notification settings - Fork 0
/
grammar1.fcfg
166 lines (130 loc) · 6.49 KB
/
grammar1.fcfg
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
%start S
###############
# Grammar Rules
###############
# TODO: Allow parentheses for explicit grouping in almost all rules
# Sentence Forms
################
S[SPEC=live,SEM=?s] -> LIVENESS[SEM=?s]
S[SPEC=safe,SEM=?s] -> SAFETY[SEM=?s]
S[SPEC=init,SEM=?s] -> INIT[SEM=?s]
S[SPEC=safe,SEM=?s] -> MEMORY[SEM=?s]
# Initial condition formulae
############################
INIT[SPEC=init,SEM=?ph] -> ENV STARTWITH PHI_ENV[SEM=?ph] | ROB STARTWITH PHI_ACT[SEM=?ph] | ROB STARTIN PHI_REG[SEM=?ph]
INIT[SPEC=init,SEM=<And(?ph1,?ph2)>] -> ROB STARTIN PHI_REG[SEM=?ph1] WITH PHI_ACT[SEM=?ph2]
# Safety formulae
#################
SAFETY[SPEC=safe,SEM=<Glob(?ph)>,PROP=?ph] -> ALWAYS PHI_ENV[SEM=?ph] | ALWAYS PHI_ROB[SEM=?ph]
SAFETY[SPEC=safe,SEM=<Glob(?s)>] -> CONDITIONAL[SPEC=safe,SEM=?s]
# Liveness formulae
###################
LIVENESS[SPEC=live,SEM=<GlobFin(?ph)>,PROP=?ph] -> INFDO PHI_ENV[SEM=?ph] | INFDO PHI_ROB[SEM=?ph]
LIVENESS[SPEC=live,SEM=<?lc(GlobFin(?ph1),GlobFin(?ph2))>] -> INFDO PHI_ROB[SEM=?ph1] LC[SEM=?lc] PHI_ROB[SEM=?ph2]
LIVENESS[SPEC=live,SEM=<And(GlobFin(?ph),Glob(Imp(?ph,?s)))>] -> GOTO PHI_ROB[SEM=?ph] ANDSTAY[SEM=?s]
LIVENESS[SPEC=live,SEM=<GlobFin(?s)>] -> CONDITIONAL[SPEC=live,SEM=?s]
# Conditional formulae
######################
# Conditionals come in one of three forms:
# 1) If [condition] then [requirement]
CONDITIONAL[SPEC=?sp,SEM=<Imp(?cond,?p)>] -> IF IC[SEM=?cond] THEN REQUIREMENT[SPEC=?sp,SEM=?req,PROP=?p]
# 2) [requirement] unless [condition]
CONDITIONAL[SPEC=?sp,SEM=<Imp(Not(?cond),?p)>] -> REQUIREMENT[SPEC=?sp,SEM=?req,PROP=?p] UNLESS IC[SEM=?cond]
# 3) [requirement] if and only iff [condition]
CONDITIONAL[SPEC=?sp,SEM=<Iff(?cond,?p)>] -> REQUIREMENT[SPEC=?sp,SEM=?req,PROP=?p] IFF IC[SEM=?cond]
# Requirements can be either a safety sentence or a liveness sentence
REQUIREMENT[SPEC=?sp,SEM=?req,PROP=?p] -> SAFETY[SPEC=?sp,SEM=?req,PROP=?p] | LIVENESS[SPEC=?sp,SEM=?req,PROP=?p]
# Conditions are independent clauses (IC) made up of either a noun phrase (NP) and verb phrase (VP)
# or two ICs conjoined by a logical connective
IC[SEM=?vp] -> NP[PER=?per] VP[PER=?per,SEM=?vp]
IC[SEM=<?lc(?ic1,?ic2)>] -> IC[SEM=?ic1] LC[SEM=?lc] IC[SEM=?ic2]
# Valid noun phrases are limited to identifiers of the robot
NP[PER=?per] -> ROB[PER=?per]
# Valid verb phrases consist of either a linking verb (LV) and a predicative expression (PE),
# a transitive verb (of either 'sense' or 'activate') and a corresponding proposition, or
# two VPs conjoined by a logical connective.
VP[PER=?per,SEM=<Next(?pe)>] -> LV[PER=?per,TEN=pres] PE[SEM=?pe]
VP[PER=?per,SEM=?pe] -> LV[PER=?per,TEN=past] PE[SEM=?pe]
VP[PER=?per,SEM=<Next(?p)>] -> SENSE[TEN=pres,PER=?per] PHI_ENV[SEM=?p] | ACTIVATE[TEN=pres,PER=?per] PHI_ACT[SEM=?p]
VP[PER=?per,SEM=?p] -> SENSE[TEN=past,PER=?per] PHI_ENV[SEM=?p] | ACTIVATE[TEN=past,PER=?per] PHI_ACT[SEM=?p]
VP[PER=?per,SEM=<?lc(?vp1,?vp2)>] -> VP[PER=?per,SEM=?vp1] LC[SEM=?lc] VP[PER=?per,SEM=?vp2]
# Valid predicative expressions are: a preposition (P) and region, a participle (of either
# 'sense' or 'activate') and a corresponding proposition, a negation (NEG) and a PE,
# or two PEs conjoined by a logical connective
PE[SEM=?r] -> P PHI_REG[SEM=?r]
PE[SEM=?p] -> SENSING PHI_ENV[SEM=?p] | ACTIVATING PHI_ACT[SEM=?p]
PE[SEM=<?n(?p)>] -> NEG[SEM=?n] PE[TEN=?t,SEM=?p]
PE[SEM=<?lc(?p1,?p2)>] -> PE[SEM=?p1] LC[SEM=?lc] PE[SEM=?p2]
# Memory proposition
MEMORY[SEM=<$Mem(?p,?s,?r)>] -> PHI_ROB[SEM=?p] SETON PHI[SEM=?s] RESETON PHI[SEM=?r]
# Toggle proposition
MEMORY[SEM=<$Tog(?p,?t)>] -> PHI_ROB[SEM=?p] TOGGLEON PHI[SEM=?t]
# Propositions
##############
PHI[SEM=?p] -> PHI_ENV[SEM=?p] | PHI_ROB[SEM=?p] | FALSE[SEM=?p]
# Environment propositions, composed of valid sensor propositions
PHI_ENV[SEM=?ph] -> SENSOR[SEM=?ph]
PHI_ENV[SEM=<?ng(?ph)>] -> NEG[SEM=?ng] PHI_ENV[SEM=?ph]
PHI_ENV[SEM=<?lc(?p1,?p2)>] -> PHI_ENV[SEM=?p1] LC[SEM=?lc] PHI_ENV[SEM=?p2]
PHI_ENV[SEM=<?a(?g)>] -> ANY[SEM=?a] SENSORGROUP[SEM=?g] | ALL[SEM=?a] SENSORGROUP[SEM=?g]
# Region propositions, composed of valid region names or quantified groups
PHI_REG[SEM=?ph] -> REGION[SEM=?ph]
PHI_REG[SEM=<?ng(?ph)>] -> NEG[SEM=?ng] PHI_REG[SEM=?ph]
PHI_REG[SEM=<?lc(?p1,?p2)>] -> PHI_REG[SEM=?p1] LC[SEM=?lc] PHI_REG[SEM=?p2]
REGION[SEM=<?a(?g)>] -> ANY[SEM=?a] GROUP[SEM=?g] | ALL[SEM=?a] GROUP[SEM=?g]
# Action propositions, composed of valid robot actions and auxilliary propositions
PHI_ACT[SEM=?ph] -> ACTION[SEM=?ph]
PHI_ACT[SEM=<?ng(?ph)>] -> NEG[SEM=?ng] PHI_ACT[SEM=?ph]
PHI_ACT[SEM=<?lc(?p1,?p2)>] -> PHI_ACT[SEM=?p1] LC[SEM=?lc] PHI_ACT[SEM=?p2]
# Robot propositions, composed of any valid proposition except sensor propositions
PHI_ROB[SEM=?ph] -> REGION[SEM=?ph]
PHI_ROB[SEM=?ph] -> ACTION[SEM=?ph]
PHI_ROB[SEM=?ph] -> AUXPROP[SEM=?ph]
PHI_ROB[SEM=<?ng(?ph)>] -> NEG[SEM=?ng] PHI_ROB[SEM=?ph]
PHI_ROB[SEM=<?lc(?p1,?p2)>] -> PHI_ROB[SEM=?p1] LC[SEM=?lc] PHI_ROB[SEM=?p2]
###############
# Lexical Rules
###############
# Fixed lexicon:
################
ACTIVATE[TEN=pres,PER=second] -> 'activate'
ACTIVATE[TEN=pres,PER=third] -> 'activates'
ACTIVATE[TEN=past,PER=second] -> 'activated'
ACTIVATE[TEN=past,PER=third] -> 'activated'
ACTIVATING[SEM=<\x.x>] -> 'activating'
ALL[SEM=<\x.$All(x)>] -> 'all'
ALWAYS[SEM=<\x.Glob(x)>] -> 'always' | 'always' 'do' | 'do'
ANDSTAY[SEM=<$stay>] -> 'and' 'stay' | 'and' 'stay' 'there'
ANY[SEM=<\x.$Any(x)>] -> 'any'
ENV[SEM=<\x.x>] -> 'environment' | 'env'
FALSE[SEM=<false>] -> 'false'
GOTO[SEM=<\x.GlobFin(x)>] -> 'go' 'to'
IF[SEM=<\x.x>] -> 'if'
IFF[SEM=<\x.x>] -> 'if' 'and' 'only' 'if' | 'iff'
INFDO[SEM=<\x.GlobFin(x)>] -> 'go' 'to' | 'visit' | 'infinitely' 'often' 'do' | 'infinitely' 'often'
LC[SEM=<\x y.Or(x,y)>] -> 'or'
LC[SEM=<\x y.And(x,y)>] -> 'and'
LV[TEN=pres,PER=third] -> 'is'
LV[TEN=pres,PER=second] -> 'are'
LV[TEN=past,PER=third] -> 'was'
LV[TEN=past,PER=second] -> 'were'
NEG[SEM=<\x.Not(x)>] -> 'not'
P[SEM=<\x.x>] -> 'in'
RESETON[SEM=<\x.x>] -> 'and' 'reset' 'on'
ROB[PER=third] -> 'robot' | 'the' 'robot'
ROB[PER=second] -> 'you'
SETON[SEM=<\x.x>] -> 'is' 'set' 'on'
SENSE[TEN=pres,PER=second] -> 'sense'
SENSE[TEN=pres,PER=third] -> 'senses'
SENSE[TEN=past,PER=second] -> 'sensed'
SENSE[TEN=past,PER=third] -> 'sensed'
SENSING[SEM=<\x.x>] -> 'sensing'
STARTWITH[SEM=<\x.x>] -> 'starts' 'with' | 'start' 'with'
STARTIN[SEM=<\x.x>] -> 'starts' 'in' | 'start' 'in'
THEN[SEM=<\x.x>] -> 'then'
TOGGLEON[SEM=<\x.x>] -> 'is' 'toggled' 'on'
TRUE[SEM=<true>] -> 'true'
UNLESS[SEM=<\x.x>] -> 'unless'
WITH[SEM=<\x.x>] -> 'with'
# Specification-determined lexicon added below:
###############################################