diff options
author | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2021-01-17 03:13:47 -0500 |
---|---|---|
committer | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2021-01-17 03:13:47 -0500 |
commit | 6ac7f9bb5a9e8c2e98960cd56ca083741a709f3f (patch) | |
tree | 2fcb033ee2cf34506b9550a9939c421babfae7dd /Domains/crossingScenario | |
parent | complete queries for lane structure (diff) | |
download | VIATRA-Generator-6ac7f9bb5a9e8c2e98960cd56ca083741a709f3f.tar.gz VIATRA-Generator-6ac7f9bb5a9e8c2e98960cd56ca083741a709f3f.tar.zst VIATRA-Generator-6ac7f9bb5a9e8c2e98960cd56ca083741a709f3f.zip |
add some actor-related queries, solve minor Z3 issue
Diffstat (limited to 'Domains/crossingScenario')
3 files changed, 137 insertions, 67 deletions
diff --git a/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig b/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig index b216ed3f..c79c5775 100644 --- a/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig +++ b/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig | |||
@@ -9,8 +9,8 @@ generate { | |||
9 | scope = { | 9 | scope = { |
10 | #node = 15..100, | 10 | #node = 15..100, |
11 | #int = {}, | 11 | #int = {}, |
12 | #<Lane> = 20..25//, | 12 | #<Lane> = 10..25, |
13 | //#<Actor> = 1..10, | 13 | #<Actor> = 10..25//, |
14 | //#<Relation> = 1..10 | 14 | //#<Relation> = 1..10 |
15 | } | 15 | } |
16 | 16 | ||
diff --git a/Domains/crossingScenario/queries/crossingScenarioQueries.vql b/Domains/crossingScenario/queries/crossingScenarioQueries.vql index ee7c0b34..352c77c0 100644 --- a/Domains/crossingScenario/queries/crossingScenarioQueries.vql +++ b/Domains/crossingScenario/queries/crossingScenarioQueries.vql | |||
@@ -11,6 +11,14 @@ import "http://www.eclipse.org/emf/2002/Ecore" | |||
11 | //} | 11 | //} |
12 | 12 | ||
13 | ////////////// | 13 | ////////////// |
14 | //CrossingScenario | ||
15 | ///////////// | ||
16 | |||
17 | //TODO Hard-code xSize? | ||
18 | //TODO Hard-code ySize? | ||
19 | //TODO Hard-code maxTime? | ||
20 | |||
21 | ////////////// | ||
14 | //Lane | 22 | //Lane |
15 | ////////////// | 23 | ////////////// |
16 | 24 | ||
@@ -154,71 +162,103 @@ pattern define_referenceCoord_laneWithPrevHasCorrectRefCoord(l:Lane) { | |||
154 | //Lane+Actor | 162 | //Lane+Actor |
155 | ////////////// | 163 | ////////////// |
156 | 164 | ||
165 | /////////Actor (a) on vertical lane (l) must have a.xPos=[l.rc, l.rc + l.nw] | ||
166 | @Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") | ||
167 | pattern define_placedOn_actorOnVerticalLane(a : Actor, vl:Lane_Vertical) { | ||
168 | Actor.placedOn(a, vl); | ||
169 | Actor.xPos(a, x); | ||
170 | Lane.referenceCoord(vl, r); | ||
171 | check(x <= r); | ||
172 | } or { | ||
173 | Actor.placedOn(a, vl); | ||
174 | Actor.xPos(a, x); | ||
175 | Lane.referenceCoord(vl, r); | ||
176 | Lane.numWidth(vl, w); | ||
177 | check(x >= (r + w)); | ||
178 | } | ||
157 | 179 | ||
158 | ////@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") | 180 | @Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") |
159 | ////pattern actorOnVerticalLane(a : Actor) { | 181 | pattern define_placedOn_actorOnHorizLane(a : Actor, hl:Lane_Horizontal) { |
160 | //// Actor.placedOn(a, l); | 182 | Actor.placedOn(a, hl); |
161 | //// Lane.orientation(l, Orientation::Vertical); | 183 | Actor.yPos(a, y); |
162 | //// Actor.xPos(a, x); | 184 | Lane.referenceCoord(hl, r); |
163 | //// Lane.referenceCoord(l, r); | 185 | check(y <= r); |
164 | //// check(x <= r); | 186 | } or { |
165 | ////} or { | 187 | Actor.placedOn(a, hl); |
166 | //// Actor.placedOn(a, l); | 188 | Actor.yPos(a, y); |
167 | //// Lane.orientation(l, Orientation::Vertical); | 189 | Lane.referenceCoord(hl, r); |
168 | //// Actor.xPos(a, x); | 190 | Lane.numWidth(hl, w); |
169 | //// Lane.referenceCoord(l, r); | 191 | check(y >= (r + w)); |
170 | //// Lane.numWidth(l, w); | 192 | } |
171 | //// check(x >= (r + w)); | 193 | |
172 | ////} | 194 | ////////////// |
173 | //// | 195 | //Actor |
174 | ////@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for horizontal lanes") | 196 | ////////////// |
175 | ////pattern actorOnHorizontalLane(a : Actor) { | 197 | |
176 | //// Actor.placedOn(a, l); | 198 | ////TODO |
177 | //// Lane.orientation(l, Orientation::Horizontal); | 199 | /////////xPos of every actor mmust be within bounds defined in CS |
178 | //// Actor.yPos(a, y); | 200 | //@Constraint(severity="error", key={l}, message="1 Actor") |
179 | //// Lane.referenceCoord(l, r); | 201 | //pattern define_actor_xPosWithinCSbounds(cs:CrossingScenario, a:Actor) { |
180 | //// check(y <= r); | 202 | // |
181 | ////} or { | 203 | //} |
182 | //// Actor.placedOn(a, l); | ||
183 | //// Lane.orientation(l, Orientation::Horizontal); | ||
184 | //// Actor.yPos(a, y); | ||
185 | //// Lane.referenceCoord(l, r); | ||
186 | //// Lane.numWidth(l, w); | ||
187 | //// check(y >= (r + w)); | ||
188 | ////} | ||
189 | // | ||
190 | ////@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation") | ||
191 | ////pattern actorOnLane(a : Actor) { | ||
192 | //// find actorOnVerticalLane(a); | ||
193 | ////// neg find actorOnHorizontalLane(a); | ||
194 | ////} | ||
195 | //// | ||
196 | ////private pattern actorOnVerticalLane(a : Actor) { | ||
197 | //// Actor.placedOn(a, l); | ||
198 | //// Lane.orientation(l, Orientation::Vertical); | ||
199 | //// Actor.xPos(a, x); | ||
200 | //// Lane.referenceCoord(l, r); | ||
201 | //// Lane.numWidth(l, w); | ||
202 | //// check(x >= r); | ||
203 | //// check(x <= (r + w)); | ||
204 | ////} | ||
205 | // | ||
206 | ////@Constraint(severity = "error", key = {l}, message = "this defines the placedOn relation") | ||
207 | ////pattern widthSpec(l : Lane) { | ||
208 | //// Lane.numWidth(l, w); | ||
209 | //// check(w != 5); | ||
210 | ////} | ||
211 | // | ||
212 | ////private pattern actorOnHorizontalLane(a : Actor) { | ||
213 | //// Actor.placedOn(a, l); | ||
214 | //// Lane.orientation(l, Orientation::Vertical); | ||
215 | //// Actor.yPos(a, y); | ||
216 | //// Lane.referenceCoord(l, r); | ||
217 | //// Lane.widthNum(l, w); | ||
218 | //// check(y >= r); | ||
219 | //// check(y <= (r + w)); | ||
220 | ////} | ||
221 | // | 204 | // |
205 | ////TODO | ||
206 | /////////yPos of every actor mmust be within bounds defined in CS | ||
207 | //@Constraint(severity="error", key={l}, message="2 Actor") | ||
208 | //pattern define_actor_yPosWithinCSbounds(cs:CrossingScenario, a:Actor) { | ||
209 | // | ||
210 | //} | ||
211 | |||
212 | |||
213 | /////////pedestrian-width (3) | ||
214 | pattern define_actor_pedestrianWidth(p:Pedestrian) { | ||
215 | Pedestrian.width(p, 1.0); | ||
216 | } | ||
217 | |||
218 | /////////pedestrian-width (4) | ||
219 | pattern define_actor_pedestrianLength(p:Pedestrian) { | ||
220 | Pedestrian.length(p, 1.0); | ||
221 | } | ||
222 | |||
223 | /////////actor-width (5) | ||
224 | pattern define_actor_actorWidth(a:Actor) { | ||
225 | Actor.placedOn(a, l); | ||
226 | Lane_Vertical(l); | ||
227 | Actor.width(p, 1.0); | ||
228 | } or { | ||
229 | Actor.placedOn(a, l); | ||
230 | Lane_Horizontal(l); | ||
231 | Actor.width(p, 3.0); | ||
232 | } | ||
233 | |||
234 | /////////actor-width (6) | ||
235 | pattern define_actor_actorLength(a:Actor) { | ||
236 | Actor.placedOn(a, l); | ||
237 | Lane_Vertical(l); | ||
238 | Actor.length(p, 3.0); | ||
239 | } or { | ||
240 | Actor.placedOn(a, l); | ||
241 | Lane_Horizontal(l); | ||
242 | Actor.length(p, 1.0); | ||
243 | } | ||
244 | |||
245 | |||
246 | /////////xSpeed of actor on verticalLane is 0 | ||
247 | @Constraint(severity="error", key={a}, message="7 Actor") | ||
248 | pattern define_actor_actorOnVertLaneHasxSpeed0(a:Actor, vl:Lane_Vertical) { | ||
249 | Actor.placedOn(a, vl); | ||
250 | Actor.xSpeed(a, xSpeed); | ||
251 | check(xSpeed != 0); | ||
252 | } | ||
253 | |||
254 | /////////ySpeed of actor on horizontalLane is 0 | ||
255 | @Constraint(severity="error", key={a}, message="8 Actor") | ||
256 | pattern define_actor_actorOnHoriLaneHasySpeed0(a:Actor, hl:Lane_Horizontal) { | ||
257 | Actor.placedOn(a, hl); | ||
258 | Actor.ySpeed(a, ySpeed); | ||
259 | check(ySpeed != 0); | ||
260 | } | ||
261 | |||
222 | //////////////// | 262 | //////////////// |
223 | ////CollisionExists | 263 | ////CollisionExists |
224 | //////////////// | 264 | //////////////// |
diff --git a/Domains/crossingScenario/src/crossingScenario/run/QueryDebug.java b/Domains/crossingScenario/src/crossingScenario/run/QueryDebug.java index 9f9b939b..51ace4b8 100644 --- a/Domains/crossingScenario/src/crossingScenario/run/QueryDebug.java +++ b/Domains/crossingScenario/src/crossingScenario/run/QueryDebug.java | |||
@@ -16,14 +16,16 @@ import org.eclipse.emf.ecore.resource.ResourceSet; | |||
16 | import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl; | 16 | import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl; |
17 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; | 17 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; |
18 | 18 | ||
19 | import crossingScenario.Actor; | ||
19 | import crossingScenario.CrossingScenario; | 20 | import crossingScenario.CrossingScenario; |
20 | import crossingScenario.CrossingScenarioPackage; | 21 | import crossingScenario.CrossingScenarioPackage; |
21 | import crossingScenario.Lane; | 22 | import crossingScenario.Lane; |
22 | 23 | ||
23 | public class QueryDebug { | 24 | public class QueryDebug { |
24 | public static void main(String[] args) throws FileNotFoundException { | 25 | public static void main(String[] args) throws FileNotFoundException { |
25 | // checkPrevLanes("outputs/models/1.xmi", "outputs/simplePrevLane.tgf"); | 26 | checkPrevLanes("outputs/models/1.xmi", "outputs/simplePrevLane.tgf"); |
26 | testOnInstance(); | 27 | // testOnInstance(); |
28 | // miniRETest("21/2"); | ||
27 | } | 29 | } |
28 | 30 | ||
29 | public static void checkPrevLanes(String pathSrc, String pathTgt) throws FileNotFoundException { | 31 | public static void checkPrevLanes(String pathSrc, String pathTgt) throws FileNotFoundException { |
@@ -35,6 +37,12 @@ public class QueryDebug { | |||
35 | PrintWriter printer = new PrintWriter(pathTgt); | 37 | PrintWriter printer = new PrintWriter(pathTgt); |
36 | 38 | ||
37 | CrossingScenario cs = ((CrossingScenario) res.getContents().get(0)); | 39 | CrossingScenario cs = ((CrossingScenario) res.getContents().get(0)); |
40 | |||
41 | for (Actor o : cs.getActors()) { | ||
42 | String nodeName = "(" + o.getXPos()+","+o.getYPos() + ")"; | ||
43 | printer.println(o.hashCode() + " " + nodeName); | ||
44 | } | ||
45 | |||
38 | for (Lane o : cs.getLanes()) { | 46 | for (Lane o : cs.getLanes()) { |
39 | String prefix = ""; | 47 | String prefix = ""; |
40 | if (cs.getHorizontal_head().equals(o) || cs.getVertical_head().equals(o)) { | 48 | if (cs.getHorizontal_head().equals(o) || cs.getVertical_head().equals(o)) { |
@@ -53,6 +61,13 @@ public class QueryDebug { | |||
53 | printer.println(curName + " " + curPrev + " " + edgeLabel); | 61 | printer.println(curName + " " + curPrev + " " + edgeLabel); |
54 | } | 62 | } |
55 | } | 63 | } |
64 | |||
65 | for (Actor o : cs.getActors()) { | ||
66 | int actName = o.hashCode(); | ||
67 | int lanName = o.getPlacedOn().hashCode(); | ||
68 | printer.println(actName + " " + lanName ); | ||
69 | } | ||
70 | |||
56 | printer.flush(); | 71 | printer.flush(); |
57 | printer.close(); | 72 | printer.close(); |
58 | System.out.println("TGF CREATED"); | 73 | System.out.println("TGF CREATED"); |
@@ -168,5 +183,20 @@ public class QueryDebug { | |||
168 | } | 183 | } |
169 | return res; | 184 | return res; |
170 | } | 185 | } |
186 | |||
187 | public static void miniRETest(String in) { | ||
188 | Double oSol = 0.0; | ||
189 | String re = "([0-9]+)/([0-9]+)"; | ||
190 | Pattern p = Pattern.compile(re); | ||
191 | Matcher ma = p.matcher(in); | ||
192 | if (ma.matches()) { | ||
193 | int numerator = Integer.parseInt(ma.group(1)); | ||
194 | int denominator = Integer.parseInt(ma.group(2)); | ||
195 | oSol = (double) numerator / denominator; | ||
196 | System.out.println(oSol); | ||
197 | } else { | ||
198 | System.err.println("Problem converting string: " + in); | ||
199 | } | ||
200 | } | ||
171 | 201 | ||
172 | } | 202 | } |