aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorLibravatar Aren Babikian <aren.babikian@mail.mcgill.ca>2021-01-19 01:15:32 +0100
committerLibravatar Aren Babikian <aren.babikian@mail.mcgill.ca>2021-01-19 01:15:32 +0100
commit598fa1dae639ac110b2f549e8c2978ae3974c53a (patch)
tree69bd6b39cdbd65833ce0f4656981ab25911c3bd1
parentadd some actor-related queries, solve minor Z3 issue (diff)
downloadVIATRA-Generator-598fa1dae639ac110b2f549e8c2978ae3974c53a.tar.gz
VIATRA-Generator-598fa1dae639ac110b2f549e8c2978ae3974c53a.tar.zst
VIATRA-Generator-598fa1dae639ac110b2f549e8c2978ae3974c53a.zip
add vsconfig flag to allow running dreal locally
Diffstat
-rw-r--r--Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend9
-rw-r--r--Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig3
-rw-r--r--Domains/crossingScenario/plugin.xml12
-rw-r--r--Domains/crossingScenario/queries/crossingScenarioQueries.vql1026
-rw-r--r--Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/plugin.xml58
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.logic.model/plugin.xml52
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java74
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/plugin.xml28
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend4
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend6
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend15
11 files changed, 672 insertions, 615 deletions
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend
index bb21f8ee..94b84bc3 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend
@@ -143,11 +143,18 @@ class SolverLoader {
143 if (config.containsKey("numeric-solver")) { 143 if (config.containsKey("numeric-solver")) {
144 val stringValue = config.get("numeric-solver") 144 val stringValue = config.get("numeric-solver")
145 c.numericSolverSelection = switch (stringValue) { 145 c.numericSolverSelection = switch (stringValue) {
146 case "dreal": NumericSolverSelection.DREAL 146 case "dreal-docker": NumericSolverSelection.DREAL_DOCKER
147 case "dreal-local": NumericSolverSelection.DREAL_LOCAL
147 case "z3": NumericSolverSelection.Z3 148 case "z3": NumericSolverSelection.Z3
148 default: throw new IllegalArgumentException("Unknown numeric solver selection: " + stringValue) 149 default: throw new IllegalArgumentException("Unknown numeric solver selection: " + stringValue)
149 } 150 }
150 } 151 }
152 if (config.containsKey("dreal-local-path")) {
153 val stringValue = config.get("dreal-local-path")
154 if (!stringValue.equals("")){
155 c.drealLocalPath = stringValue;
156 }
157 }
151 if (config.containsKey("scopePropagator")) { 158 if (config.containsKey("scopePropagator")) {
152 val stringValue = config.get("scopePropagator") 159 val stringValue = config.get("scopePropagator")
153 c.scopePropagatorStrategy = switch (stringValue) { 160 c.scopePropagatorStrategy = switch (stringValue) {
diff --git a/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig b/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig
index c79c5775..7f62377e 100644
--- a/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig
+++ b/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig
@@ -4,7 +4,7 @@ import viatra "queries/crossingScenarioQueries.vql"
4generate { 4generate {
5 metamodel = { package crossingScenario } 5 metamodel = { package crossingScenario }
6 constraints = { package queries} 6 constraints = { package queries}
7 partial-model = { "inputs/CrossingScenarioInit.xmi"} 7 partial-model = { "inputs/crossingScenarioInit.xmi"}
8 solver = ViatraSolver 8 solver = ViatraSolver
9 scope = { 9 scope = {
10 #node = 15..100, 10 #node = 15..100,
@@ -18,6 +18,7 @@ generate {
18 runtime = 10000, 18 runtime = 10000,
19 log-level = normal, 19 log-level = normal,
20 "numeric-solver" = "z3", 20 "numeric-solver" = "z3",
21 "dreal-local-path" = "/home/models/dreal4/bazel-bin/dreal/dreal",
21 "scopePropagator" = "typeHierarchy"} 22 "scopePropagator" = "typeHierarchy"}
22 23
23 runs = 1 24 runs = 1
diff --git a/Domains/crossingScenario/plugin.xml b/Domains/crossingScenario/plugin.xml
index 6a1c7f69..c8846e1b 100644
--- a/Domains/crossingScenario/plugin.xml
+++ b/Domains/crossingScenario/plugin.xml
@@ -1,7 +1,7 @@
1<?xml version="1.0" encoding="UTF-8"?><?eclipse version="3.0"?><!-- 1<?xml version="1.0" encoding="UTF-8"?><?eclipse version="3.0"?><!--
2--><plugin> 2--><plugin>
3 <extension point="org.eclipse.emf.ecore.generated_package"> 3 <extension point="org.eclipse.emf.ecore.generated_package">
4 <!-- @generated crossingScenario --> 4 <!-- @generated crossingScenario -->
5 <package class="crossingScenario.CrossingScenarioPackage" genModel="model/crossingScenario.genmodel" uri="http://www.example.com/crossingScenario"/> 5 <package class="crossingScenario.CrossingScenarioPackage" genModel="model/crossingScenario.genmodel" uri="http://www.example.com/crossingScenario"/>
6 </extension> 6 </extension>
7</plugin> 7</plugin>
diff --git a/Domains/crossingScenario/queries/crossingScenarioQueries.vql b/Domains/crossingScenario/queries/crossingScenarioQueries.vql
index 352c77c0..f8bcc92c 100644
--- a/Domains/crossingScenario/queries/crossingScenarioQueries.vql
+++ b/Domains/crossingScenario/queries/crossingScenarioQueries.vql
@@ -1,514 +1,514 @@
1package queries 1package queries
2 2
3import "http://www.example.com/crossingScenario" 3import "http://www.example.com/crossingScenario"
4import "http://www.eclipse.org/emf/2002/Ecore" 4import "http://www.eclipse.org/emf/2002/Ecore"
5 5
6//////Minimal Failing Example 6//////Minimal Failing Example
7//@Constraint(severity = "error", key = {l}, message = "this defines the placedOn relation") 7//@Constraint(severity = "error", key = {l}, message = "this defines the placedOn relation")
8//pattern patterThatOnlyWorksWithInt(l : Lane) { 8//pattern patterThatOnlyWorksWithInt(l : Lane) {
9// Lane.referenceCoord(l, w); 9// Lane.referenceCoord(l, w);
10// check(w <= 0-10.0); 10// check(w <= 0-10.0);
11//} 11//}
12 12
13////////////// 13//////////////
14//CrossingScenario 14//CrossingScenario
15///////////// 15/////////////
16 16
17//TODO Hard-code xSize? 17//TODO Hard-code xSize?
18//TODO Hard-code ySize? 18//TODO Hard-code ySize?
19//TODO Hard-code maxTime? 19//TODO Hard-code maxTime?
20 20
21////////////// 21//////////////
22//Lane 22//Lane
23////////////// 23//////////////
24 24
25@Constraint(severity="error", key={l}, message="1 Lane") 25@Constraint(severity="error", key={l}, message="1 Lane")
26pattern define_numWidth_small(l : Lane) { 26pattern define_numWidth_small(l : Lane) {
27 Lane.width(l, Size::S_Small); 27 Lane.width(l, Size::S_Small);
28 Lane.numWidth(l, nw); 28 Lane.numWidth(l, nw);
29 check(nw <= 5.0); 29 check(nw <= 5.0);
30} or { 30} or {
31 Lane.width(l, Size::S_Small); 31 Lane.width(l, Size::S_Small);
32 Lane.numWidth(l, nw); 32 Lane.numWidth(l, nw);
33 check(nw >= 10.0); 33 check(nw >= 10.0);
34} 34}
35 35
36@Constraint(severity="error", key={l}, message="2 Lane") 36@Constraint(severity="error", key={l}, message="2 Lane")
37pattern define_numWidth_medium(l : Lane) { 37pattern define_numWidth_medium(l : Lane) {
38 Lane.width(l, ::S_Med); 38 Lane.width(l, ::S_Med);
39 Lane.numWidth(l, nw); 39 Lane.numWidth(l, nw);
40 check(nw <= 10.0); 40 check(nw <= 10.0);
41} 41}
42or { 42or {
43 Lane.width(l, Size::S_Med); 43 Lane.width(l, Size::S_Med);
44 Lane.numWidth(l, nw); 44 Lane.numWidth(l, nw);
45 check(nw >= 15.0); 45 check(nw >= 15.0);
46} 46}
47 47
48@Constraint(severity="error", key={l}, message="3 Lane") 48@Constraint(severity="error", key={l}, message="3 Lane")
49pattern define_numWidth_large(l : Lane) { 49pattern define_numWidth_large(l : Lane) {
50 Lane.width(l, Size::S_Large); 50 Lane.width(l, Size::S_Large);
51 Lane.numWidth(l, nw); 51 Lane.numWidth(l, nw);
52 check(nw <= 15.0); 52 check(nw <= 15.0);
53} 53}
54or { 54or {
55 Lane.width(l, Size::S_Large); 55 Lane.width(l, Size::S_Large);
56 Lane.numWidth(l, nw); 56 Lane.numWidth(l, nw);
57 check(nw >= 20.0); 57 check(nw >= 20.0);
58} 58}
59 59
60/////////////Prevlane 60/////////////Prevlane
61 61
62////////head lanes do not have prevLane 62////////head lanes do not have prevLane
63@Constraint(severity="error", key={l}, message="6.1 Lane") 63@Constraint(severity="error", key={l}, message="6.1 Lane")
64pattern define_prevLane_headVertLaneDoesNotHavePrevLane(cs:CrossingScenario, l:Lane_Vertical) { 64pattern define_prevLane_headVertLaneDoesNotHavePrevLane(cs:CrossingScenario, l:Lane_Vertical) {
65 CrossingScenario.vertical_head(cs, l); 65 CrossingScenario.vertical_head(cs, l);
66 Lane.prevLane(l, _); 66 Lane.prevLane(l, _);
67} 67}
68 68
69@Constraint(severity="error", key={l}, message="6.2 Lane") 69@Constraint(severity="error", key={l}, message="6.2 Lane")
70pattern define_prevLane_headHoriLaneDoesNotHavePrevLane(cs:CrossingScenario, l:Lane_Horizontal) { 70pattern define_prevLane_headHoriLaneDoesNotHavePrevLane(cs:CrossingScenario, l:Lane_Horizontal) {
71 CrossingScenario.horizontal_head(cs, l); 71 CrossingScenario.horizontal_head(cs, l);
72 Lane.prevLane(l, _); 72 Lane.prevLane(l, _);
73} 73}
74 74
75////////Non-head lanes must have prevLane 75////////Non-head lanes must have prevLane
76@Constraint(severity="error", key={l}, message="6.1 Lane") 76@Constraint(severity="error", key={l}, message="6.1 Lane")
77pattern define_prevLane_nonheadVertLaneHasPrevLane(l:Lane_Vertical) { 77pattern define_prevLane_nonheadVertLaneHasPrevLane(l:Lane_Vertical) {
78 neg find find_headVertLane(l); 78 neg find find_headVertLane(l);
79 neg find find_laneWithPrevLane(l); 79 neg find find_laneWithPrevLane(l);
80} 80}
81 81
82@Constraint(severity="error", key={l}, message="6.1 Lane") 82@Constraint(severity="error", key={l}, message="6.1 Lane")
83pattern define_prevLane_nonheadHoriLaneHasPrevLane(l:Lane_Horizontal) { 83pattern define_prevLane_nonheadHoriLaneHasPrevLane(l:Lane_Horizontal) {
84 neg find find_headHoriLane(l); 84 neg find find_headHoriLane(l);
85 neg find find_laneWithPrevLane(l); 85 neg find find_laneWithPrevLane(l);
86} 86}
87 87
88private pattern find_headVertLane(l:Lane_Vertical) { 88private pattern find_headVertLane(l:Lane_Vertical) {
89 CrossingScenario.vertical_head(_, l); 89 CrossingScenario.vertical_head(_, l);
90} 90}
91private pattern find_headHoriLane(l:Lane_Horizontal) { 91private pattern find_headHoriLane(l:Lane_Horizontal) {
92 CrossingScenario.horizontal_head(_, l); 92 CrossingScenario.horizontal_head(_, l);
93} 93}
94private pattern find_laneWithPrevLane(l:Lane) { 94private pattern find_laneWithPrevLane(l:Lane) {
95 Lane.prevLane(l, _); 95 Lane.prevLane(l, _);
96} 96}
97 97
98/////////Lane cannot be its own recursive prevLane 98/////////Lane cannot be its own recursive prevLane
99@Constraint(severity="error", key={l}, message="6.1 Lane") 99@Constraint(severity="error", key={l}, message="6.1 Lane")
100pattern define_prevLane_lanecannotBeItsOwnPrevLane(l:Lane) { 100pattern define_prevLane_lanecannotBeItsOwnPrevLane(l:Lane) {
101 Lane.prevLane(l, l); 101 Lane.prevLane(l, l);
102} 102}
103 103
104@Constraint(severity="error", key={l}, message="6.2 Lane") 104@Constraint(severity="error", key={l}, message="6.2 Lane")
105pattern define_prevLane_lanecannotBeItsOwnRecursivePrevLane(l:Lane) { 105pattern define_prevLane_lanecannotBeItsOwnRecursivePrevLane(l:Lane) {
106 find find_prevLane+(l, l); 106 find find_prevLane+(l, l);
107} 107}
108private pattern find_prevLane(l1:Lane, l2:Lane) { 108private pattern find_prevLane(l1:Lane, l2:Lane) {
109 Lane.prevLane(l1, l2); 109 Lane.prevLane(l1, l2);
110} 110}
111 111
112//////Lane cannot be prevLane of >1 other lane 112//////Lane cannot be prevLane of >1 other lane
113@Constraint(severity="error", key={l1, l2}, message="7 Lane") 113@Constraint(severity="error", key={l1, l2}, message="7 Lane")
114pattern define_prevLane_lanecannotbeprevLaneof2lanes(l1:Lane, l2:Lane) { 114pattern define_prevLane_lanecannotbeprevLaneof2lanes(l1:Lane, l2:Lane) {
115 Lane.prevLane(l1, l); 115 Lane.prevLane(l1, l);
116 Lane.prevLane(l2, l); 116 Lane.prevLane(l2, l);
117 l1 != l2; 117 l1 != l2;
118} 118}
119 119
120//////consecutive lanes must have same orientation 120//////consecutive lanes must have same orientation
121@Constraint(severity="error", key={l1, l2}, message="8 Lane") 121@Constraint(severity="error", key={l1, l2}, message="8 Lane")
122pattern define_prevLane_consecutiveLanesMustHaveSameOrientation1(l1:Lane_Horizontal, l2:Lane_Vertical) { 122pattern define_prevLane_consecutiveLanesMustHaveSameOrientation1(l1:Lane_Horizontal, l2:Lane_Vertical) {
123 Lane.prevLane(l1, l2); 123 Lane.prevLane(l1, l2);
124} 124}
125 125
126@Constraint(severity="error", key={l1, l2}, message="8 Lane") 126@Constraint(severity="error", key={l1, l2}, message="8 Lane")
127pattern define_prevLane_consecutiveLanesMustHaveSameOrientation2(l1:Lane_Vertical, l2:Lane_Horizontal) { 127pattern define_prevLane_consecutiveLanesMustHaveSameOrientation2(l1:Lane_Vertical, l2:Lane_Horizontal) {
128 Lane.prevLane(l1, l2); 128 Lane.prevLane(l1, l2);
129} 129}
130 130
131/////////////ReferenceCoord 131/////////////ReferenceCoord
132 132
133/////refCoord of head lanes must be 0 133/////refCoord of head lanes must be 0
134@Constraint(severity="error", key={l}, message="6.2 Lane") 134@Constraint(severity="error", key={l}, message="6.2 Lane")
135pattern define_prevLane_headHoriLaneHas0RefCoord(cs:CrossingScenario, l:Lane_Horizontal) { 135pattern define_prevLane_headHoriLaneHas0RefCoord(cs:CrossingScenario, l:Lane_Horizontal) {
136 CrossingScenario.horizontal_head(cs, l); 136 CrossingScenario.horizontal_head(cs, l);
137 Lane.referenceCoord(l, rc); 137 Lane.referenceCoord(l, rc);
138 check(rc != 0.0); 138 check(rc != 0.0);
139} 139}
140 140
141@Constraint(severity="error", key={l}, message="6.2 Lane") 141@Constraint(severity="error", key={l}, message="6.2 Lane")
142pattern define_prevLane_headVertLaneHas0RefCoord(cs:CrossingScenario, l:Lane_Vertical) { 142pattern define_prevLane_headVertLaneHas0RefCoord(cs:CrossingScenario, l:Lane_Vertical) {
143 CrossingScenario.vertical_head(cs, l); 143 CrossingScenario.vertical_head(cs, l);
144 Lane.referenceCoord(l, rc); 144 Lane.referenceCoord(l, rc);
145 check(rc != 0.0); 145 check(rc != 0.0);
146} 146}
147 147
148//////refCoord of a lane is prevLane.rc + curLane.numWidth 148//////refCoord of a lane is prevLane.rc + curLane.numWidth
149 149
150@Constraint(severity="error", key={l}, message="6.2 Lane") 150@Constraint(severity="error", key={l}, message="6.2 Lane")
151pattern define_referenceCoord_laneWithPrevHasCorrectRefCoord(l:Lane) { 151pattern define_referenceCoord_laneWithPrevHasCorrectRefCoord(l:Lane) {
152 Lane.prevLane(l, prev); 152 Lane.prevLane(l, prev);
153 Lane.referenceCoord(l, rcCur); 153 Lane.referenceCoord(l, rcCur);
154 154
155 Lane.numWidth(prev, wPrev); 155 Lane.numWidth(prev, wPrev);
156 Lane.referenceCoord(prev, rcPrev); 156 Lane.referenceCoord(prev, rcPrev);
157 check(rcCur != rcPrev + wPrev); 157 check(rcCur != rcPrev + wPrev);
158} 158}
159 159
160 160
161////////////// 161//////////////
162//Lane+Actor 162//Lane+Actor
163////////////// 163//////////////
164 164
165/////////Actor (a) on vertical lane (l) must have a.xPos=[l.rc, l.rc + l.nw] 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") 166@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes")
167pattern define_placedOn_actorOnVerticalLane(a : Actor, vl:Lane_Vertical) { 167pattern define_placedOn_actorOnVerticalLane(a : Actor, vl:Lane_Vertical) {
168 Actor.placedOn(a, vl); 168 Actor.placedOn(a, vl);
169 Actor.xPos(a, x); 169 Actor.xPos(a, x);
170 Lane.referenceCoord(vl, r); 170 Lane.referenceCoord(vl, r);
171 check(x <= r); 171 check(x <= r);
172} or { 172} or {
173 Actor.placedOn(a, vl); 173 Actor.placedOn(a, vl);
174 Actor.xPos(a, x); 174 Actor.xPos(a, x);
175 Lane.referenceCoord(vl, r); 175 Lane.referenceCoord(vl, r);
176 Lane.numWidth(vl, w); 176 Lane.numWidth(vl, w);
177 check(x >= (r + w)); 177 check(x >= (r + w));
178} 178}
179 179
180@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")
181pattern define_placedOn_actorOnHorizLane(a : Actor, hl:Lane_Horizontal) { 181pattern define_placedOn_actorOnHorizLane(a : Actor, hl:Lane_Horizontal) {
182 Actor.placedOn(a, hl); 182 Actor.placedOn(a, hl);
183 Actor.yPos(a, y); 183 Actor.yPos(a, y);
184 Lane.referenceCoord(hl, r); 184 Lane.referenceCoord(hl, r);
185 check(y <= r); 185 check(y <= r);
186} or { 186} or {
187 Actor.placedOn(a, hl); 187 Actor.placedOn(a, hl);
188 Actor.yPos(a, y); 188 Actor.yPos(a, y);
189 Lane.referenceCoord(hl, r); 189 Lane.referenceCoord(hl, r);
190 Lane.numWidth(hl, w); 190 Lane.numWidth(hl, w);
191 check(y >= (r + w)); 191 check(y >= (r + w));
192} 192}
193 193
194////////////// 194//////////////
195//Actor 195//Actor
196////////////// 196//////////////
197 197
198////TODO 198////TODO
199/////////xPos of every actor mmust be within bounds defined in CS 199/////////xPos of every actor mmust be within bounds defined in CS
200//@Constraint(severity="error", key={l}, message="1 Actor") 200//@Constraint(severity="error", key={l}, message="1 Actor")
201//pattern define_actor_xPosWithinCSbounds(cs:CrossingScenario, a:Actor) { 201//pattern define_actor_xPosWithinCSbounds(cs:CrossingScenario, a:Actor) {
202// 202//
203//} 203//}
204// 204//
205////TODO 205////TODO
206/////////yPos of every actor mmust be within bounds defined in CS 206/////////yPos of every actor mmust be within bounds defined in CS
207//@Constraint(severity="error", key={l}, message="2 Actor") 207//@Constraint(severity="error", key={l}, message="2 Actor")
208//pattern define_actor_yPosWithinCSbounds(cs:CrossingScenario, a:Actor) { 208//pattern define_actor_yPosWithinCSbounds(cs:CrossingScenario, a:Actor) {
209// 209//
210//} 210//}
211 211
212 212
213/////////pedestrian-width (3) 213/////////pedestrian-width (3)
214pattern define_actor_pedestrianWidth(p:Pedestrian) { 214//pattern define_actor_pedestrianWidth(p:Pedestrian) {
215 Pedestrian.width(p, 1.0); 215// Pedestrian.width(p, 1.0);
216} 216//}
217 217//
218/////////pedestrian-width (4) 218///////////pedestrian-width (4)
219pattern define_actor_pedestrianLength(p:Pedestrian) { 219//pattern define_actor_pedestrianLength(p:Pedestrian) {
220 Pedestrian.length(p, 1.0); 220// Pedestrian.length(p, 1.0);
221} 221//}
222 222
223/////////actor-width (5) 223///////////actor-width (5)
224pattern define_actor_actorWidth(a:Actor) { 224//pattern define_actor_actorWidth(a:Actor) {
225 Actor.placedOn(a, l); 225// Actor.placedOn(a, l);
226 Lane_Vertical(l); 226// Lane_Vertical(l);
227 Actor.width(p, 1.0); 227// Actor.width(p, 1.0);
228} or { 228//} or {
229 Actor.placedOn(a, l); 229// Actor.placedOn(a, l);
230 Lane_Horizontal(l); 230// Lane_Horizontal(l);
231 Actor.width(p, 3.0); 231// Actor.width(p, 3.0);
232} 232//}
233 233//
234/////////actor-width (6) 234///////////actor-width (6)
235pattern define_actor_actorLength(a:Actor) { 235//pattern define_actor_actorLength(a:Actor) {
236 Actor.placedOn(a, l); 236// Actor.placedOn(a, l);
237 Lane_Vertical(l); 237// Lane_Vertical(l);
238 Actor.length(p, 3.0); 238// Actor.length(p, 3.0);
239} or { 239//} or {
240 Actor.placedOn(a, l); 240// Actor.placedOn(a, l);
241 Lane_Horizontal(l); 241// Lane_Horizontal(l);
242 Actor.length(p, 1.0); 242// Actor.length(p, 1.0);
243} 243//}
244 244
245 245
246/////////xSpeed of actor on verticalLane is 0 246/////////xSpeed of actor on verticalLane is 0
247@Constraint(severity="error", key={a}, message="7 Actor") 247@Constraint(severity="error", key={a}, message="7 Actor")
248pattern define_actor_actorOnVertLaneHasxSpeed0(a:Actor, vl:Lane_Vertical) { 248pattern define_actor_actorOnVertLaneHasxSpeed0(a:Actor, vl:Lane_Vertical) {
249 Actor.placedOn(a, vl); 249 Actor.placedOn(a, vl);
250 Actor.xSpeed(a, xSpeed); 250 Actor.xSpeed(a, xSpeed);
251 check(xSpeed != 0); 251 check(xSpeed != 0);
252} 252}
253 253
254/////////ySpeed of actor on horizontalLane is 0 254/////////ySpeed of actor on horizontalLane is 0
255@Constraint(severity="error", key={a}, message="8 Actor") 255@Constraint(severity="error", key={a}, message="8 Actor")
256pattern define_actor_actorOnHoriLaneHasySpeed0(a:Actor, hl:Lane_Horizontal) { 256pattern define_actor_actorOnHoriLaneHasySpeed0(a:Actor, hl:Lane_Horizontal) {
257 Actor.placedOn(a, hl); 257 Actor.placedOn(a, hl);
258 Actor.ySpeed(a, ySpeed); 258 Actor.ySpeed(a, ySpeed);
259 check(ySpeed != 0); 259 check(ySpeed != 0);
260} 260}
261 261
262//////////////// 262////////////////
263////CollisionExists 263////CollisionExists
264//////////////// 264////////////////
265// 265//
266//@Constraint(severity="error", key={c}, message="x") 266//@Constraint(severity="error", key={c}, message="x")
267//pattern collisionExists_timeWithinBound(ss:CrossingScenario, c:CollisionExists) { 267//pattern collisionExists_timeWithinBound(ss:CrossingScenario, c:CollisionExists) {
268// CrossingScenario.actors.relations(ss, c); 268// CrossingScenario.actors.relations(ss, c);
269// CrossingScenario.maxTime(ss, maxTime); 269// CrossingScenario.maxTime(ss, maxTime);
270// CollisionExists. collisionTime(c, cTime); 270// CollisionExists. collisionTime(c, cTime);
271// check(cTime >= maxTime);} 271// check(cTime >= maxTime);}
272// 272//
273//@Constraint(severity="error", key={c}, message="x") 273//@Constraint(severity="error", key={c}, message="x")
274//pattern collisionExists_timeNotNegative(c:CollisionExists) { 274//pattern collisionExists_timeNotNegative(c:CollisionExists) {
275// CollisionExists. collisionTime(c, cTime); 275// CollisionExists. collisionTime(c, cTime);
276// check(cTime <= 0);} 276// check(cTime <= 0);}
277// 277//
278//@Constraint(severity="error", key={a1, c}, message="x") 278//@Constraint(severity="error", key={a1, c}, message="x")
279//pattern collisionExists_defineCollision_y1(a1:Actor, a2:Actor, c:CollisionExists) { 279//pattern collisionExists_defineCollision_y1(a1:Actor, a2:Actor, c:CollisionExists) {
280// Actor.relations(a1, c); 280// Actor.relations(a1, c);
281// CollisionExists.target(c, a2); 281// CollisionExists.target(c, a2);
282// 282//
283// Actor.length(a1, l1); 283// Actor.length(a1, l1);
284// Actor.yPos(a1, yPos1); 284// Actor.yPos(a1, yPos1);
285// Actor.ySpeed(a1, ySpeed1); 285// Actor.ySpeed(a1, ySpeed1);
286// Actor.length(a2, l2); 286// Actor.length(a2, l2);
287// Actor.yPos(a2, yPos2); 287// Actor.yPos(a2, yPos2);
288// Actor.ySpeed(a2, ySpeed2); 288// Actor.ySpeed(a2, ySpeed2);
289// CollisionExists. collisionTime(c, cTime); 289// CollisionExists. collisionTime(c, cTime);
290// //check(y_1_bottom > y_2_top 290// //check(y_1_bottom > y_2_top
291// check((yPos1 + (ySpeed1 * cTime)) - (l1/2) > (yPos2 + (ySpeed2 * cTime)) + (l2/2)); 291// check((yPos1 + (ySpeed1 * cTime)) - (l1/2) > (yPos2 + (ySpeed2 * cTime)) + (l2/2));
292//} 292//}
293// 293//
294//@Constraint(severity="error", key={a1, c}, message="x") 294//@Constraint(severity="error", key={a1, c}, message="x")
295//pattern collisionExists_defineCollision_y2(a1:Actor, a2:Actor, c:CollisionExists) { 295//pattern collisionExists_defineCollision_y2(a1:Actor, a2:Actor, c:CollisionExists) {
296// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 296// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
297// Actor.relations(a1, c); 297// Actor.relations(a1, c);
298// CollisionExists.target(c, a2); 298// CollisionExists.target(c, a2);
299// 299//
300// Actor.length(a1, l1); 300// Actor.length(a1, l1);
301// Actor.yPos(a1, yPos1); 301// Actor.yPos(a1, yPos1);
302// Actor.ySpeed(a1, ySpeed1); 302// Actor.ySpeed(a1, ySpeed1);
303// Actor.length(a2, l2); 303// Actor.length(a2, l2);
304// Actor.yPos(a2, yPos2); 304// Actor.yPos(a2, yPos2);
305// Actor.ySpeed(a2, ySpeed2); 305// Actor.ySpeed(a2, ySpeed2);
306// CollisionExists. collisionTime(c, cTime); 306// CollisionExists. collisionTime(c, cTime);
307// //check(y_1_top < y_2_bottom) 307// //check(y_1_top < y_2_bottom)
308// check((yPos1 + (ySpeed1 * cTime)) + (l1/2) < (yPos2 + (ySpeed2 * cTime)) - (l2/2)); 308// check((yPos1 + (ySpeed1 * cTime)) + (l1/2) < (yPos2 + (ySpeed2 * cTime)) - (l2/2));
309//} 309//}
310// 310//
311//@Constraint(severity="error", key={a1, c}, message="x") 311//@Constraint(severity="error", key={a1, c}, message="x")
312//pattern collisionExists_defineCollision_x1(a1:Actor, a2:Actor, c:CollisionExists) { 312//pattern collisionExists_defineCollision_x1(a1:Actor, a2:Actor, c:CollisionExists) {
313// Actor.relations(a1, c); 313// Actor.relations(a1, c);
314// CollisionExists.target(c, a2); 314// CollisionExists.target(c, a2);
315// 315//
316// Actor.width(a1, w1); 316// Actor.width(a1, w1);
317// Actor.xPos(a1, xPos1); 317// Actor.xPos(a1, xPos1);
318// Actor.xSpeed(a1, xSpeed1); 318// Actor.xSpeed(a1, xSpeed1);
319// Actor.width(a2, w2); 319// Actor.width(a2, w2);
320// Actor.xPos(a2, xPos2); 320// Actor.xPos(a2, xPos2);
321// Actor.xSpeed(a2, xSpeed2); 321// Actor.xSpeed(a2, xSpeed2);
322// CollisionExists. collisionTime(c, cTime); 322// CollisionExists. collisionTime(c, cTime);
323// //check(x_1_left > x_2_right) 323// //check(x_1_left > x_2_right)
324// check((xPos1 + (xSpeed1 * cTime)) - (w1/2) > (xPos2 + (xSpeed2 * cTime)) + (w2/2)); 324// check((xPos1 + (xSpeed1 * cTime)) - (w1/2) > (xPos2 + (xSpeed2 * cTime)) + (w2/2));
325//} 325//}
326// 326//
327//@Constraint(severity="error", key={a1, c}, message="x") 327//@Constraint(severity="error", key={a1, c}, message="x")
328//pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor, c:CollisionExists) { 328//pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor, c:CollisionExists) {
329// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 329// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
330// Actor.relations(a1, c); 330// Actor.relations(a1, c);
331// CollisionExists.target(c, a2); 331// CollisionExists.target(c, a2);
332// 332//
333// Actor.width(a1, w1); 333// Actor.width(a1, w1);
334// Actor.xPos(a1, xPos1); 334// Actor.xPos(a1, xPos1);
335// Actor.xSpeed(a1, xSpeed1); 335// Actor.xSpeed(a1, xSpeed1);
336// Actor.width(a2, w2); 336// Actor.width(a2, w2);
337// Actor.xPos(a2, xPos2); 337// Actor.xPos(a2, xPos2);
338// Actor.xSpeed(a2, xSpeed2); 338// Actor.xSpeed(a2, xSpeed2);
339// CollisionExists. collisionTime(c, cTime); 339// CollisionExists. collisionTime(c, cTime);
340// //check(x_1_right < x_2_left) 340// //check(x_1_right < x_2_left)
341// check((xPos1 + (xSpeed1 * cTime)) + (w1/2) < (xPos2 + (xSpeed2 * cTime)) - (w2/2)); 341// check((xPos1 + (xSpeed1 * cTime)) + (w1/2) < (xPos2 + (xSpeed2 * cTime)) - (w2/2));
342//} 342//}
343// 343//
344//////////////// 344////////////////
345////SeparationDistance 345////SeparationDistance
346//////////////// 346////////////////
347//@Constraint(severity="error", key={a1, sd}, message="x") 347//@Constraint(severity="error", key={a1, sd}, message="x")
348//pattern SeparationDistance_near_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { 348//pattern SeparationDistance_near_lb(a1:Actor, a2:Actor, sd:SeparationDistance) {
349// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 349// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
350// Actor.relations(a1, sd); 350// Actor.relations(a1, sd);
351// SeparationDistance.target(sd, a2); 351// SeparationDistance.target(sd, a2);
352// SeparationDistance.distance(sd, Distance::Near); 352// SeparationDistance.distance(sd, Distance::Near);
353// 353//
354// Actor.xPos(a1, x1); 354// Actor.xPos(a1, x1);
355// Actor.yPos(a1, y1); 355// Actor.yPos(a1, y1);
356// Actor.xPos(a2, x2); 356// Actor.xPos(a2, x2);
357// Actor.yPos(a2, y2); 357// Actor.yPos(a2, y2);
358// //check(dx^2 + dy^2 < 5^2) 358// //check(dx^2 + dy^2 < 5^2)
359// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 5*5); 359// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 5*5);
360//} 360//}
361// 361//
362//@Constraint(severity="error", key={a1, sd}, message="x") 362//@Constraint(severity="error", key={a1, sd}, message="x")
363//pattern SeparationDistance_near_ub(a1:Actor, a2:Actor, sd:SeparationDistance) { 363//pattern SeparationDistance_near_ub(a1:Actor, a2:Actor, sd:SeparationDistance) {
364// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 364// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
365// Actor.relations(a1, sd); 365// Actor.relations(a1, sd);
366// SeparationDistance.target(sd, a2); 366// SeparationDistance.target(sd, a2);
367// SeparationDistance.distance(sd, Distance::Near); 367// SeparationDistance.distance(sd, Distance::Near);
368// 368//
369// Actor.xPos(a1, x1); 369// Actor.xPos(a1, x1);
370// Actor.yPos(a1, y1); 370// Actor.yPos(a1, y1);
371// Actor.xPos(a2, x2); 371// Actor.xPos(a2, x2);
372// Actor.yPos(a2, y2); 372// Actor.yPos(a2, y2);
373// //check(dx^2 + dy^2 > 10^2) 373// //check(dx^2 + dy^2 > 10^2)
374// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10); 374// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10);
375//} 375//}
376// 376//
377//@Constraint(severity="error", key={a1, sd}, message="x") 377//@Constraint(severity="error", key={a1, sd}, message="x")
378//pattern SeparationDistance_medium_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { 378//pattern SeparationDistance_medium_lb(a1:Actor, a2:Actor, sd:SeparationDistance) {
379// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 379// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
380// Actor.relations(a1, sd); 380// Actor.relations(a1, sd);
381// SeparationDistance.target(sd, a2); 381// SeparationDistance.target(sd, a2);
382// SeparationDistance.distance(sd, Distance::Medium); 382// SeparationDistance.distance(sd, Distance::Medium);
383// 383//
384// Actor.xPos(a1, x1); 384// Actor.xPos(a1, x1);
385// Actor.yPos(a1, y1); 385// Actor.yPos(a1, y1);
386// Actor.xPos(a2, x2); 386// Actor.xPos(a2, x2);
387// Actor.yPos(a2, y2); 387// Actor.yPos(a2, y2);
388// //check(dx^2 + dy^2 < 10^2) 388// //check(dx^2 + dy^2 < 10^2)
389// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10); 389// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10);
390//} 390//}
391// 391//
392//@Constraint(severity="error", key={a1, sd}, message="x") 392//@Constraint(severity="error", key={a1, sd}, message="x")
393//pattern SeparationDistance_medium_ub(a1:Actor, a2:Actor, sd:SeparationDistance) { 393//pattern SeparationDistance_medium_ub(a1:Actor, a2:Actor, sd:SeparationDistance) {
394// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 394// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
395// Actor.relations(a1, sd); 395// Actor.relations(a1, sd);
396// SeparationDistance.target(sd, a2); 396// SeparationDistance.target(sd, a2);
397// SeparationDistance.distance(sd, Distance::Medium); 397// SeparationDistance.distance(sd, Distance::Medium);
398// 398//
399// Actor.xPos(a1, x1); 399// Actor.xPos(a1, x1);
400// Actor.yPos(a1, y1); 400// Actor.yPos(a1, y1);
401// Actor.xPos(a2, x2); 401// Actor.xPos(a2, x2);
402// Actor.yPos(a2, y2); 402// Actor.yPos(a2, y2);
403// //check(dx^2 + dy^2 > 1^2) 403// //check(dx^2 + dy^2 > 1^2)
404// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 15*15); 404// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 15*15);
405//} 405//}
406// 406//
407//@Constraint(severity="error", key={a1, sd}, message="x") 407//@Constraint(severity="error", key={a1, sd}, message="x")
408//pattern SeparationDistance_far_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { 408//pattern SeparationDistance_far_lb(a1:Actor, a2:Actor, sd:SeparationDistance) {
409// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 409// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
410// Actor.relations(a1, sd); 410// Actor.relations(a1, sd);
411// SeparationDistance.target(sd, a2); 411// SeparationDistance.target(sd, a2);
412// SeparationDistance.distance(sd, Distance::Far); 412// SeparationDistance.distance(sd, Distance::Far);
413// 413//
414// Actor.xPos(a1, x1); 414// Actor.xPos(a1, x1);
415// Actor.yPos(a1, y1); 415// Actor.yPos(a1, y1);
416// Actor.xPos(a2, x2); 416// Actor.xPos(a2, x2);
417// Actor.yPos(a2, y2); 417// Actor.yPos(a2, y2);
418// //check(dx^2 + dy^2 < 15^2) 418// //check(dx^2 + dy^2 < 15^2)
419// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); 419// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15);
420//} 420//}
421// 421//
422//////////////// 422////////////////
423////CollisionDoesNotExist 423////CollisionDoesNotExist
424//////////////// 424////////////////
425// 425//
426////@Constraint(severity="error", key={a1, cdne}, message="x") 426////@Constraint(severity="error", key={a1, cdne}, message="x")
427////pattern collisionDoesNotExist(a1:Actor, a2:Actor, ss:CrossingScenario, cdne:CollisionDoesNotExist) { 427////pattern collisionDoesNotExist(a1:Actor, a2:Actor, ss:CrossingScenario, cdne:CollisionDoesNotExist) {
428//// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 428//// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
429//// 429////
430//// CrossingScenario.actors(ss, a1); 430//// CrossingScenario.actors(ss, a1);
431//// CrossingScenario.actors(ss, a2); 431//// CrossingScenario.actors(ss, a2);
432//// Actor.relations(a1, cdne); 432//// Actor.relations(a1, cdne);
433//// CollisionDoesNotExist.target(cdne, a2); 433//// CollisionDoesNotExist.target(cdne, a2);
434//// CrossingScenario.maxTime(ss, maxTime); 434//// CrossingScenario.maxTime(ss, maxTime);
435//// 435////
436//// Actor.width(a1, w1); 436//// Actor.width(a1, w1);
437//// Actor.length(a1, l1); 437//// Actor.length(a1, l1);
438//// Actor.xPos(a1, xPos1); 438//// Actor.xPos(a1, xPos1);
439//// Actor.yPos(a1, yPos1); 439//// Actor.yPos(a1, yPos1);
440//// Actor.xSpeed(a1, xSpeed1); 440//// Actor.xSpeed(a1, xSpeed1);
441//// Actor.ySpeed(a1, ySpeed1); 441//// Actor.ySpeed(a1, ySpeed1);
442//// 442////
443//// Actor.width(a2, w2); 443//// Actor.width(a2, w2);
444//// Actor.length(a2, l2); 444//// Actor.length(a2, l2);
445//// Actor.xPos(a2, xPos2); 445//// Actor.xPos(a2, xPos2);
446//// Actor.yPos(a2, yPos2); 446//// Actor.yPos(a2, yPos2);
447//// Actor.xSpeed(a2, xSpeed2); 447//// Actor.xSpeed(a2, xSpeed2);
448//// Actor.ySpeed(a2, ySpeed2); 448//// Actor.ySpeed(a2, ySpeed2);
449//// //check(dx^2 + dy^2 < 15^2) 449//// //check(dx^2 + dy^2 < 15^2)
450//// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); 450//// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15);
451////} 451////}
452// 452//
453//////////////// 453////////////////
454////VisionBlocked 454////VisionBlocked
455//////////////// 455////////////////
456// 456//
457////OPTIONS 1: everything is from a single check expression containing ITEs 457////OPTIONS 1: everything is from a single check expression containing ITEs
458////Currently unhandled bygenerator 458////Currently unhandled bygenerator
459//@Constraint(severity="error", key={a1, vb}, message="x") 459//@Constraint(severity="error", key={a1, vb}, message="x")
460//pattern visionBlocked_ites_top(a1:Actor, a2:Actor, vb:VisionBlocked) { 460//pattern visionBlocked_ites_top(a1:Actor, a2:Actor, vb:VisionBlocked) {
461// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 461// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
462// Actor.relations(a1, vb); 462// Actor.relations(a1, vb);
463// VisionBlocked.target(vb, a2); 463// VisionBlocked.target(vb, a2);
464// VisionBlocked.blockedBy(vb, aBlocker); 464// VisionBlocked.blockedBy(vb, aBlocker);
465// 465//
466// Actor.xPos(a1, x1); 466// Actor.xPos(a1, x1);
467// Actor.yPos(a1, y1); 467// Actor.yPos(a1, y1);
468// Actor.xPos(a2, x2); 468// Actor.xPos(a2, x2);
469// Actor.yPos(a2, y2); 469// Actor.yPos(a2, y2);
470// Actor.xPos(aBlocker, xBlocker); 470// Actor.xPos(aBlocker, xBlocker);
471// Actor.yPos(aBlocker, yBlocker); 471// Actor.yPos(aBlocker, yBlocker);
472// Actor.length(aBlocker, lenBlocker); 472// Actor.length(aBlocker, lenBlocker);
473// Actor.width(aBlocker, widBlocker); 473// Actor.width(aBlocker, widBlocker);
474// 474//
475// //check(slope of a1-to-BlockerTop < slope of a1-to-a2) 475// //check(slope of a1-to-BlockerTop < slope of a1-to-a2)
476// check( 476// check(
477// ( yBlocker - y1 + (if(xBlocker > x1){lenBlocker/2}else{0-lenBlocker/2})) / 477// ( yBlocker - y1 + (if(xBlocker > x1){lenBlocker/2}else{0-lenBlocker/2})) /
478// ( xBlocker - x1 + (if(yBlocker > y1){0-widBlocker/2}else{widBlocker/2})) 478// ( xBlocker - x1 + (if(yBlocker > y1){0-widBlocker/2}else{widBlocker/2}))
479// < ((y1-y2)/(x1-x2))); 479// < ((y1-y2)/(x1-x2)));
480//} 480//}
481// 481//
482//@Constraint(severity="error", key={a1, vb}, message="x") 482//@Constraint(severity="error", key={a1, vb}, message="x")
483//pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor, vb:VisionBlocked) { 483//pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor, vb:VisionBlocked) {
484// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 484// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
485// Actor.relations(a1, vb); 485// Actor.relations(a1, vb);
486// VisionBlocked.target(vb, a2); 486// VisionBlocked.target(vb, a2);
487// VisionBlocked.blockedBy(vb, aBlocker); 487// VisionBlocked.blockedBy(vb, aBlocker);
488// 488//
489// Actor.xPos(a1, x1); 489// Actor.xPos(a1, x1);
490// Actor.yPos(a1, y1); 490// Actor.yPos(a1, y1);
491// Actor.xPos(a2, x2); 491// Actor.xPos(a2, x2);
492// Actor.yPos(a2, y2); 492// Actor.yPos(a2, y2);
493// Actor.xPos(aBlocker, xBlocker); 493// Actor.xPos(aBlocker, xBlocker);
494// Actor.yPos(aBlocker, yBlocker); 494// Actor.yPos(aBlocker, yBlocker);
495// Actor.length(aBlocker, lenBlocker); 495// Actor.length(aBlocker, lenBlocker);
496// Actor.width(aBlocker, widBlocker); 496// Actor.width(aBlocker, widBlocker);
497// 497//
498// //check(slope of a1-to-BlockerBottom > slope of a1-to-a2) 498// //check(slope of a1-to-BlockerBottom > slope of a1-to-a2)
499// check( 499// check(
500// ( yBlocker - y1 + (if(xBlocker > x1){0-lenBlocker/2}else{lenBlocker/2})) / 500// ( yBlocker - y1 + (if(xBlocker > x1){0-lenBlocker/2}else{lenBlocker/2})) /
501// ( xBlocker - x1 + (if(yBlocker > y1){widBlocker/2}else{0-widBlocker/2})) 501// ( xBlocker - x1 + (if(yBlocker > y1){widBlocker/2}else{0-widBlocker/2}))
502// > ((y1-y2)/(x1-x2))); 502// > ((y1-y2)/(x1-x2)));
503//} 503//}
504// 504//
505////OPTION 2: 505////OPTION 2:
506////we handle ITE by seperating the constraints 506////we handle ITE by seperating the constraints
507// 507//
508////This will involve 1 constarint for each decision path, but will require multiple check expressions within the same pattern 508////This will involve 1 constarint for each decision path, but will require multiple check expressions within the same pattern
509// 509//
510////OPTION 3: 510////OPTION 3:
511////If this is nott working still, we will have to add some strctural components to the MM 511////If this is nott working still, we will have to add some strctural components to the MM
512////to differentiate the different cases and reduce the requirements of if, then, else 512////to differentiate the different cases and reduce the requirements of if, then, else
513// 513//
514////This will involve more patterns, and some that are pstructural as well. \ No newline at end of file 514////This will involve more patterns, and some that are pstructural as well. \ No newline at end of file
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/plugin.xml b/Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/plugin.xml
index 1f192d67..419d8640 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/plugin.xml
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/plugin.xml
@@ -1,30 +1,30 @@
1<?xml version="1.0" encoding="UTF-8"?><?eclipse version="3.0"?><!-- 1<?xml version="1.0" encoding="UTF-8"?><?eclipse version="3.0"?><!--
2--><plugin> 2--><plugin>
3 <extension point="org.eclipse.emf.ecore.generated_package"> 3 <extension point="org.eclipse.emf.ecore.generated_package">
4 <!-- @generated satellite --> 4 <!-- @generated satellite -->
5 <package class="satellite.SatellitePackage" genModel="model/satellite.genmodel" uri="http://www.example.org/satellite"/> 5 <package class="satellite.SatellitePackage" genModel="model/satellite.genmodel" uri="http://www.example.org/satellite"/>
6 </extension> 6 </extension>
7 <extension id="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.SatelliteQueries" point="org.eclipse.viatra.query.runtime.queryspecification"> 7 <extension id="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.SatelliteQueries" point="org.eclipse.viatra.query.runtime.queryspecification">
8 <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:hu.bme.mit.inf.dslreasoner.domains.satellite.queries.SatelliteQueries" id="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.SatelliteQueries"> 8 <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:hu.bme.mit.inf.dslreasoner.domains.satellite.queries.SatelliteQueries" id="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.SatelliteQueries">
9 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.communicationLinkDoesNotStartAtContainingElement"/> 9 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.communicationLinkDoesNotStartAtContainingElement"/>
10 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.transmittingGroundStationNetwork"/> 10 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.transmittingGroundStationNetwork"/>
11 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.roundStationNetworkUHF"/> 11 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.roundStationNetworkUHF"/>
12 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.notEnoughInterferometryPayloads"/> 12 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.notEnoughInterferometryPayloads"/>
13 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.communicationLoop"/> 13 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.communicationLoop"/>
14 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.incompatibleSourceAndTargetBand"/> 14 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.incompatibleSourceAndTargetBand"/>
15 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.threeUCubeSatWithNonUhfCrossLink"/> 15 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.threeUCubeSatWithNonUhfCrossLink"/>
16 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.cubeSatWithKaAntenna"/> 16 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.cubeSatWithKaAntenna"/>
17 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.smallSat"/> 17 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.smallSat"/>
18 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.differentFrequency"/> 18 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.differentFrequency"/>
19 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.tooHighFrequencyForUHF"/> 19 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.tooHighFrequencyForUHF"/>
20 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.tooLowFrequencyForUHF"/> 20 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.tooLowFrequencyForUHF"/>
21 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.tooHighFrequencyForKaComm"/> 21 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.tooHighFrequencyForKaComm"/>
22 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.tooLowFrequencyForKaComm"/> 22 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.tooLowFrequencyForKaComm"/>
23 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.tooHighFrequencyForXComm"/> 23 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.tooHighFrequencyForXComm"/>
24 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.tooLowFrequencyForXComm"/> 24 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.tooLowFrequencyForXComm"/>
25 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.tooHighPathLengthForSatelite"/> 25 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.tooHighPathLengthForSatelite"/>
26 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.tooLowPathLengthForSatelite"/> 26 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.tooLowPathLengthForSatelite"/>
27 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.tooLowPathLengthForGroundStation"/> 27 <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.satellite.queries.tooLowPathLengthForGroundStation"/>
28 </group> 28 </group>
29 </extension> 29 </extension>
30</plugin> 30</plugin>
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/plugin.xml b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/plugin.xml
index 413002e2..bad09614 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/plugin.xml
+++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/plugin.xml
@@ -1,27 +1,27 @@
1<?xml version="1.0" encoding="UTF-8"?><?eclipse version="3.0"?><!-- 1<?xml version="1.0" encoding="UTF-8"?><?eclipse version="3.0"?><!--
2--><plugin> 2--><plugin>
3 <extension point="org.eclipse.emf.ecore.generated_package"> 3 <extension point="org.eclipse.emf.ecore.generated_package">
4 <!-- @generated logiclanguage --> 4 <!-- @generated logiclanguage -->
5 <package class="hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage" genModel="model/logiclanguage.genmodel" uri="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language"/> 5 <package class="hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage" genModel="model/logiclanguage.genmodel" uri="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language"/>
6 </extension> 6 </extension>
7 <extension point="org.eclipse.emf.ecore.generated_package"> 7 <extension point="org.eclipse.emf.ecore.generated_package">
8 <!-- @generated logiclanguage --> 8 <!-- @generated logiclanguage -->
9 <package class="hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage" genModel="model/logiclanguage.genmodel" uri="http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem"/> 9 <package class="hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage" genModel="model/logiclanguage.genmodel" uri="http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem"/>
10 </extension> 10 </extension>
11 <extension point="org.eclipse.emf.ecore.generated_package"> 11 <extension point="org.eclipse.emf.ecore.generated_package">
12 <!-- @generated logiclanguage --> 12 <!-- @generated logiclanguage -->
13 <package class="hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultPackage" genModel="model/logiclanguage.genmodel" uri="http://www.bme.hu/mit/inf/dslreasoner/logic/model/result"/> 13 <package class="hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultPackage" genModel="model/logiclanguage.genmodel" uri="http://www.bme.hu/mit/inf/dslreasoner/logic/model/result"/>
14 </extension> 14 </extension>
15 <extension id="hu.bme.mit.inf.dslreasoner.logic.model.patterns.TypeUtil" point="org.eclipse.viatra.query.runtime.queryspecification"> 15 <extension id="hu.bme.mit.inf.dslreasoner.logic.model.patterns.TypeUtil" point="org.eclipse.viatra.query.runtime.queryspecification">
16 <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:hu.bme.mit.inf.dslreasoner.logic.model.patterns.TypeUtil" id="hu.bme.mit.inf.dslreasoner.logic.model.patterns.TypeUtil"> 16 <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:hu.bme.mit.inf.dslreasoner.logic.model.patterns.TypeUtil" id="hu.bme.mit.inf.dslreasoner.logic.model.patterns.TypeUtil">
17 <query-specification fqn="hu.bme.mit.inf.dslreasoner.logic.model.patterns.supertypeStar"/> 17 <query-specification fqn="hu.bme.mit.inf.dslreasoner.logic.model.patterns.supertypeStar"/>
18 <query-specification fqn="hu.bme.mit.inf.dslreasoner.logic.model.patterns.typeDirectElements"/> 18 <query-specification fqn="hu.bme.mit.inf.dslreasoner.logic.model.patterns.typeDirectElements"/>
19 <query-specification fqn="hu.bme.mit.inf.dslreasoner.logic.model.patterns.possibleDynamicType"/> 19 <query-specification fqn="hu.bme.mit.inf.dslreasoner.logic.model.patterns.possibleDynamicType"/>
20 <query-specification fqn="hu.bme.mit.inf.dslreasoner.logic.model.patterns.mustTypeElement"/> 20 <query-specification fqn="hu.bme.mit.inf.dslreasoner.logic.model.patterns.mustTypeElement"/>
21 <query-specification fqn="hu.bme.mit.inf.dslreasoner.logic.model.patterns.typeSystemIsInconsistent"/> 21 <query-specification fqn="hu.bme.mit.inf.dslreasoner.logic.model.patterns.typeSystemIsInconsistent"/>
22 <query-specification fqn="hu.bme.mit.inf.dslreasoner.logic.model.patterns.elementNotDefinedInSupertype"/> 22 <query-specification fqn="hu.bme.mit.inf.dslreasoner.logic.model.patterns.elementNotDefinedInSupertype"/>
23 <query-specification fqn="hu.bme.mit.inf.dslreasoner.logic.model.patterns.elementWithNoPossibleDynamicType"/> 23 <query-specification fqn="hu.bme.mit.inf.dslreasoner.logic.model.patterns.elementWithNoPossibleDynamicType"/>
24 <query-specification fqn="hu.bme.mit.inf.dslreasoner.logic.model.patterns.cyclicTypeHierarchy"/> 24 <query-specification fqn="hu.bme.mit.inf.dslreasoner.logic.model.patterns.cyclicTypeHierarchy"/>
25 </group> 25 </group>
26 </extension> 26 </extension>
27</plugin> 27</plugin>
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java
index f6c0bc71..1ce3af06 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java
@@ -7,6 +7,7 @@ import java.io.FileInputStream;
7import java.io.IOException; 7import java.io.IOException;
8import java.io.InputStream; 8import java.io.InputStream;
9import java.io.InputStreamReader; 9import java.io.InputStreamReader;
10import java.io.PrintWriter;
10import java.util.ArrayList; 11import java.util.ArrayList;
11import java.util.Arrays; 12import java.util.Arrays;
12import java.util.HashMap; 13import java.util.HashMap;
@@ -28,43 +29,53 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par
28import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement; 29import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement;
29 30
30public class NumericDrealProblemSolver extends NumericProblemSolver{ 31public class NumericDrealProblemSolver extends NumericProblemSolver{
32
33 private final boolean useDocker;
31 34
32 private final String containerName; 35 private String containerName = "<container-name-here>";
36 private String drealLocalPath = "<path-to-dreal-here>";
33 private final String smtFileName = "tmp/smt.smt2"; 37 private final String smtFileName = "tmp/smt.smt2";
34 private Map<Object, String> varMap; 38 private Map<Object, String> varMap;
35 private Map<String, String> curVar2Decl; 39 private Map<String, String> curVar2Decl;
40
41 private final int TIMEOUT_DOCKER = 5;
42 private final int TIMEOUT_LOCAL = 2;
36 43
37 public NumericDrealProblemSolver() throws IOException, InterruptedException { 44 public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath) throws IOException, InterruptedException {
45 this.useDocker = useDocker;
46 this.varMap = new HashMap<Object, String>();
47 this.drealLocalPath = drealLocalPath;
48
49 if (useDocker) setupDocker();
50 }
51
52 private void setupDocker() throws IOException, InterruptedException {
38 //setup docker 53 //setup docker
39 //TODO ENSURE that container name is not already in use???? 54 //TODO ENSURE that container name is not already in use????
40 //TODO if dreal/dreal4 image is not downloaded, download it. 55 //TODO if dreal/dreal4 image is not downloaded, download it.
41 File tempDir = new File(System.getProperty("java.io.tmpdir")); 56 this.containerName = UUID.randomUUID().toString().replace("-", "");
42 containerName = UUID.randomUUID().toString().replace("-", "");
43 List<String> startDocker = new ArrayList<String>( 57 List<String> startDocker = new ArrayList<String>(
44 Arrays.asList("docker", "run", 58 Arrays.asList("docker", "run",
45 "-id", "--rm", 59 "-id", "--rm",
46 "--name", containerName, 60 "--name", containerName,
47// "-p", "8080:80", 61// "-p", "8080:80",
48 "dreal/dreal4")); 62 "dreal/dreal4"));
49 runProcess(startDocker); 63 runProcess(startDocker, TIMEOUT_DOCKER);
50
51 //setup varmap
52 varMap = new HashMap<Object, String>();
53 } 64 }
54 65
55 private Process runProcess(List<String> cmd) throws IOException, InterruptedException { 66 private Process runProcess(List<String> cmd, int timeout) throws IOException, InterruptedException {
56 String s = String.join(" ", cmd); 67 String s = String.join(" ", cmd);
57 Process p = Runtime.getRuntime().exec(s); 68 Process p = Runtime.getRuntime().exec(s);
58// p.waitFor(); 69// p.waitFor();
59 //TODO timeout if needed 70 //TODO timeout if needed
60 if (!p.waitFor(5, TimeUnit.SECONDS)) { 71 if (!p.waitFor(timeout, TimeUnit.SECONDS)) {
61 p.destroy(); 72 p.destroy();
62 System.err.println("TIMEOUT"); //DEBUG 73 System.err.println("TIMEOUT"); //DEBUG
63 } 74 }
64 return p; 75 return p;
65 } 76 }
66 77
67 private Process callDreal(List<String> numProbContents, boolean getModel) throws IOException, InterruptedException { 78 private Process callDrealDocker(List<String> numProbContents, boolean getModel) throws IOException, InterruptedException {
68 String numProbContentStr = String.join("\\n", numProbContents); 79 String numProbContentStr = String.join("\\n", numProbContents);
69 List<String> drealCmd = new ArrayList<String>(Arrays.asList( 80 List<String> drealCmd = new ArrayList<String>(Arrays.asList(
70 "docker", "exec", containerName, 81 "docker", "exec", containerName,
@@ -78,7 +89,28 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
78 if (getModel) {drealCmd.add("--model");} 89 if (getModel) {drealCmd.add("--model");}
79 drealCmd.add(smtFileName + "\""); 90 drealCmd.add(smtFileName + "\"");
80 91
81 return runProcess(drealCmd); 92 return runProcess(drealCmd, TIMEOUT_DOCKER);
93 }
94
95 private Process callDrealLocal(List<String> numProbContents, boolean getModel) throws IOException, InterruptedException {
96 //print numProbConents to temp file
97 File tempFile = File.createTempFile("smt", ".smt2");
98
99 PrintWriter printer = new PrintWriter(tempFile);
100 for (String s : numProbContents) {
101 printer.println(s);
102 }
103 printer.close();
104
105 //call local dreal with path to temp file
106 List<String> drealCmd = new ArrayList<String>();
107 drealCmd.add(drealLocalPath);
108 if (getModel) {drealCmd.add("--model");}
109 drealCmd.add(tempFile.getAbsolutePath());
110
111 System.out.println(drealCmd);
112
113 return runProcess(drealCmd, TIMEOUT_LOCAL);
82 } 114 }
83 115
84 private List<String> getDrealStream(InputStream stream) throws IOException { 116 private List<String> getDrealStream(InputStream stream) throws IOException {
@@ -262,6 +294,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
262 } 294 }
263 } 295 }
264 296
297 @SuppressWarnings("unused")
265 private void printOutput(List<String> list) { 298 private void printOutput(List<String> list) {
266 for (String line : list) { 299 for (String line : list) {
267 System.out.println(line); 300 System.out.println(line);
@@ -282,7 +315,11 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
282 315
283 //CALL DREAL 316 //CALL DREAL
284 long startSolvingProblem = System.nanoTime(); 317 long startSolvingProblem = System.nanoTime();
285 Process outputProcess = callDreal(numProbContent, false); 318
319 Process outputProcess;
320 if (this.useDocker) outputProcess = callDrealDocker(numProbContent, false);
321 else outputProcess = callDrealLocal(numProbContent, false);
322
286 List<List<String>> outputs = getProcessOutput(outputProcess); 323 List<List<String>> outputs = getProcessOutput(outputProcess);
287 boolean result = getDrealResult(outputProcess.exitValue(), outputs); 324 boolean result = getDrealResult(outputProcess.exitValue(), outputs);
288 endSolvingProblem = System.nanoTime()-startSolvingProblem; 325 endSolvingProblem = System.nanoTime()-startSolvingProblem;
@@ -320,10 +357,15 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
320 long startformingProblem = System.nanoTime(); 357 long startformingProblem = System.nanoTime();
321 List<String> numProbContent = formNumericProblemInstance(matches); 358 List<String> numProbContent = formNumericProblemInstance(matches);
322 endformingProblem = System.nanoTime()-startformingProblem; 359 endformingProblem = System.nanoTime()-startformingProblem;
323 360
361
324 //CALL DREAL 362 //CALL DREAL
325 long startSolvingProblem = System.nanoTime(); 363 long startSolvingProblem = System.nanoTime();
326 Process outputProcess = callDreal(numProbContent, true); 364
365 Process outputProcess;
366 if (this.useDocker) outputProcess = callDrealDocker(numProbContent, false);
367 else outputProcess = callDrealLocal(numProbContent, false);
368
327 List<List<String>> outputs = getProcessOutput(outputProcess); 369 List<List<String>> outputs = getProcessOutput(outputProcess);
328 boolean result = getDrealResult(outputProcess.exitValue(), outputs); 370 boolean result = getDrealResult(outputProcess.exitValue(), outputs);
329 endSolvingProblem = System.nanoTime()-startSolvingProblem; 371 endSolvingProblem = System.nanoTime()-startSolvingProblem;
@@ -373,7 +415,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
373 public void teardown() throws IOException, InterruptedException { 415 public void teardown() throws IOException, InterruptedException {
374 List<String> stopDocker = new ArrayList<String>( 416 List<String> stopDocker = new ArrayList<String>(
375 Arrays.asList("docker", "stop", containerName)); 417 Arrays.asList("docker", "stop", containerName));
376 runProcess(stopDocker); 418 runProcess(stopDocker, TIMEOUT_DOCKER);
377 //TODO Check if above went well? 419 //TODO Check if above went well?
378 } 420 }
379 421
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/plugin.xml b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/plugin.xml
index 05e00983..6e4d96ca 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/plugin.xml
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/plugin.xml
@@ -1,14 +1,14 @@
1<?xml version="1.0" encoding="UTF-8"?><plugin> 1<?xml version="1.0" encoding="UTF-8"?><plugin>
2 <extension id="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.TypeAnalysis" point="org.eclipse.viatra.query.runtime.queryspecification"> 2 <extension id="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.TypeAnalysis" point="org.eclipse.viatra.query.runtime.queryspecification">
3 <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.TypeAnalysis" id="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.TypeAnalysis"> 3 <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.TypeAnalysis" id="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.TypeAnalysis">
4 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.hasDefinedSupertype"/> 4 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.hasDefinedSupertype"/>
5 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.dontHaveDefinedSupertype"/> 5 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.dontHaveDefinedSupertype"/>
6 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.newElementTypeConstructor"/> 6 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.newElementTypeConstructor"/>
7 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.newElementTypeRefinementTarget"/> 7 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.newElementTypeRefinementTarget"/>
8 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.incompatibleSuperType"/> 8 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.incompatibleSuperType"/>
9 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.incompatibleTopType"/> 9 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.incompatibleTopType"/>
10 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.newElementTypeRefinementNegativeConstraint"/> 10 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.newElementTypeRefinementNegativeConstraint"/>
11 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.newElementMayTypeNegativeConstraint"/> 11 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.newElementMayTypeNegativeConstraint"/>
12 </group> 12 </group>
13 </extension> 13 </extension>
14</plugin> 14</plugin>
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
index d386241d..ed04ae4a 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
@@ -165,8 +165,8 @@ class ViatraReasoner extends LogicReasoner {
165 val solverTime = System.nanoTime - solverStartTime 165 val solverTime = System.nanoTime - solverStartTime
166 viatraConfig.progressMonitor.workedSearchFinished 166 viatraConfig.progressMonitor.workedSearchFinished
167 167
168 //dreal teardown 168 //dreal docker teardown
169 if (viatraConfig.numericSolverSelection == NumericSolverSelection.DREAL){ 169 if (viatraConfig.numericSolverSelection == NumericSolverSelection.DREAL_DOCKER){
170 (numericSolver.numericSolverSelection as NumericDrealProblemSolver).teardown() 170 (numericSolver.numericSolverSelection as NumericDrealProblemSolver).teardown()
171 } 171 }
172 172
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
index ebfd5d81..c0daaad2 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
@@ -34,7 +34,8 @@ enum PunishSizeStrategy {
34} 34}
35 35
36enum NumericSolverSelection { 36enum NumericSolverSelection {
37 DREAL, 37 DREAL_DOCKER,
38 DREAL_LOCAL,
38 Z3 39 Z3
39} 40}
40 41
@@ -75,7 +76,8 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration {
75 public var nonContainmentWeight = 1 76 public var nonContainmentWeight = 1
76 public var unfinishedWFWeight = 1 77 public var unfinishedWFWeight = 1
77 public var calculateObjectCreationCosts = false 78 public var calculateObjectCreationCosts = false
78 public var numericSolverSelection = NumericSolverSelection.DREAL //currently defaulted to DREAL 79 public var numericSolverSelection = NumericSolverSelection.DREAL_DOCKER //currently defaulted to DREAL
80 public var drealLocalPath = "<path-to-dreal>";
79 81
80 public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral( 82 public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral(
81 PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp) 83 PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp)
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
index ab3e6601..9223ecc8 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
@@ -34,6 +34,7 @@ class NumericSolver {
34 val boolean intermediateConsistencyCheck 34 val boolean intermediateConsistencyCheck
35 val boolean caching; 35 val boolean caching;
36 Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap 36 Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap
37 val String drealLocalPath;
37 38
38 var long runtime = 0 39 var long runtime = 0
39 var long cachingTime = 0 40 var long cachingTime = 0
@@ -43,12 +44,16 @@ class NumericSolver {
43 new(ModelGenerationMethod method, ViatraReasonerConfiguration config, boolean caching) { 44 new(ModelGenerationMethod method, ViatraReasonerConfiguration config, boolean caching) {
44 this.method = method 45 this.method = method
45 this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks 46 this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks
46 this.t = new NumericTranslator(createNumericTranslator(config.numericSolverSelection))
47 this.caching = caching 47 this.caching = caching
48 this.drealLocalPath = config.drealLocalPath
49 this.t = new NumericTranslator(createNumericTranslator(config.numericSolverSelection))
48 } 50 }
49 51
50 def createNumericTranslator(NumericSolverSelection solverSelection) { 52 def createNumericTranslator(NumericSolverSelection solverSelection) {
51 if (solverSelection == NumericSolverSelection.DREAL) return new NumericDrealProblemSolver 53 if (solverSelection == NumericSolverSelection.DREAL_DOCKER)
54 return new NumericDrealProblemSolver(true, null)
55 if (solverSelection == NumericSolverSelection.DREAL_LOCAL)
56 return new NumericDrealProblemSolver(false, drealLocalPath)
52 if (solverSelection == NumericSolverSelection.Z3) return new NumericZ3ProblemSolver 57 if (solverSelection == NumericSolverSelection.Z3) return new NumericZ3ProblemSolver
53 } 58 }
54 59
@@ -98,12 +103,12 @@ class NumericSolver {
98 finalResult=true 103 finalResult=true
99 } else { 104 } else {
100 val propagatedConstraints = new HashMap 105 val propagatedConstraints = new HashMap
101 println("------ Any matches?") 106 println("<<<<START-STEP>>>>")
102 for(entry : matches.entrySet) { 107 for(entry : matches.entrySet) {
103 val constraint = entry.key 108 val constraint = entry.key
104 println("------ " + constraint) 109// println("--match?-- " + constraint)
105 val allMatches = entry.value.allMatches.map[it.toArray] 110 val allMatches = entry.value.allMatches.map[it.toArray]
106 println("------ " + allMatches.toList) 111// println("---------- " + entry.value.allMatches)
107 propagatedConstraints.put(constraint,allMatches) 112 propagatedConstraints.put(constraint,allMatches)
108 } 113 }
109 if(propagatedConstraints.values.forall[empty]) { 114 if(propagatedConstraints.values.forall[empty]) {
generated by cgit v1.2.3 (git 2.25.1) at 2024-04-25 15:26:21 +0000