From 598fa1dae639ac110b2f549e8c2978ae3974c53a Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Tue, 19 Jan 2021 01:15:32 +0100 Subject: add vsconfig flag to allow running dreal locally --- .../application/execution/SolverLoader.xtend | 9 +- .../inputs/crossingScenarioGen.vsconfig | 3 +- Domains/crossingScenario/plugin.xml | 12 +- .../queries/crossingScenarioQueries.vql | 1026 ++++++++++---------- .../plugin.xml | 58 +- .../plugin.xml | 52 +- .../viatra2logic/NumericDrealProblemSolver.java | 74 +- .../plugin.xml | 28 +- .../viatrasolver/reasoner/ViatraReasoner.xtend | 4 +- .../reasoner/ViatraReasonerConfiguration.xtend | 6 +- .../viatrasolver/reasoner/dse/NumericSolver.xtend | 15 +- 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 { if (config.containsKey("numeric-solver")) { val stringValue = config.get("numeric-solver") c.numericSolverSelection = switch (stringValue) { - case "dreal": NumericSolverSelection.DREAL + case "dreal-docker": NumericSolverSelection.DREAL_DOCKER + case "dreal-local": NumericSolverSelection.DREAL_LOCAL case "z3": NumericSolverSelection.Z3 default: throw new IllegalArgumentException("Unknown numeric solver selection: " + stringValue) } } + if (config.containsKey("dreal-local-path")) { + val stringValue = config.get("dreal-local-path") + if (!stringValue.equals("")){ + c.drealLocalPath = stringValue; + } + } if (config.containsKey("scopePropagator")) { val stringValue = config.get("scopePropagator") 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" generate { metamodel = { package crossingScenario } constraints = { package queries} - partial-model = { "inputs/CrossingScenarioInit.xmi"} + partial-model = { "inputs/crossingScenarioInit.xmi"} solver = ViatraSolver scope = { #node = 15..100, @@ -18,6 +18,7 @@ generate { runtime = 10000, log-level = normal, "numeric-solver" = "z3", + "dreal-local-path" = "/home/models/dreal4/bazel-bin/dreal/dreal", "scopePropagator" = "typeHierarchy"} 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 @@ - - - - - +--> + + + + + 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 @@ -package queries - -import "http://www.example.com/crossingScenario" -import "http://www.eclipse.org/emf/2002/Ecore" - -//////Minimal Failing Example -//@Constraint(severity = "error", key = {l}, message = "this defines the placedOn relation") -//pattern patterThatOnlyWorksWithInt(l : Lane) { -// Lane.referenceCoord(l, w); -// check(w <= 0-10.0); -//} - -////////////// -//CrossingScenario -///////////// - -//TODO Hard-code xSize? -//TODO Hard-code ySize? -//TODO Hard-code maxTime? - -////////////// -//Lane -////////////// - -@Constraint(severity="error", key={l}, message="1 Lane") -pattern define_numWidth_small(l : Lane) { - Lane.width(l, Size::S_Small); - Lane.numWidth(l, nw); - check(nw <= 5.0); -} or { - Lane.width(l, Size::S_Small); - Lane.numWidth(l, nw); - check(nw >= 10.0); -} - -@Constraint(severity="error", key={l}, message="2 Lane") -pattern define_numWidth_medium(l : Lane) { - Lane.width(l, ::S_Med); - Lane.numWidth(l, nw); - check(nw <= 10.0); -} -or { - Lane.width(l, Size::S_Med); - Lane.numWidth(l, nw); - check(nw >= 15.0); -} - -@Constraint(severity="error", key={l}, message="3 Lane") -pattern define_numWidth_large(l : Lane) { - Lane.width(l, Size::S_Large); - Lane.numWidth(l, nw); - check(nw <= 15.0); -} -or { - Lane.width(l, Size::S_Large); - Lane.numWidth(l, nw); - check(nw >= 20.0); -} - -/////////////Prevlane - -////////head lanes do not have prevLane -@Constraint(severity="error", key={l}, message="6.1 Lane") -pattern define_prevLane_headVertLaneDoesNotHavePrevLane(cs:CrossingScenario, l:Lane_Vertical) { - CrossingScenario.vertical_head(cs, l); - Lane.prevLane(l, _); -} - -@Constraint(severity="error", key={l}, message="6.2 Lane") -pattern define_prevLane_headHoriLaneDoesNotHavePrevLane(cs:CrossingScenario, l:Lane_Horizontal) { - CrossingScenario.horizontal_head(cs, l); - Lane.prevLane(l, _); -} - -////////Non-head lanes must have prevLane -@Constraint(severity="error", key={l}, message="6.1 Lane") -pattern define_prevLane_nonheadVertLaneHasPrevLane(l:Lane_Vertical) { - neg find find_headVertLane(l); - neg find find_laneWithPrevLane(l); -} - -@Constraint(severity="error", key={l}, message="6.1 Lane") -pattern define_prevLane_nonheadHoriLaneHasPrevLane(l:Lane_Horizontal) { - neg find find_headHoriLane(l); - neg find find_laneWithPrevLane(l); -} - -private pattern find_headVertLane(l:Lane_Vertical) { - CrossingScenario.vertical_head(_, l); -} -private pattern find_headHoriLane(l:Lane_Horizontal) { - CrossingScenario.horizontal_head(_, l); -} -private pattern find_laneWithPrevLane(l:Lane) { - Lane.prevLane(l, _); -} - -/////////Lane cannot be its own recursive prevLane -@Constraint(severity="error", key={l}, message="6.1 Lane") -pattern define_prevLane_lanecannotBeItsOwnPrevLane(l:Lane) { - Lane.prevLane(l, l); -} - -@Constraint(severity="error", key={l}, message="6.2 Lane") -pattern define_prevLane_lanecannotBeItsOwnRecursivePrevLane(l:Lane) { - find find_prevLane+(l, l); -} -private pattern find_prevLane(l1:Lane, l2:Lane) { - Lane.prevLane(l1, l2); -} - -//////Lane cannot be prevLane of >1 other lane -@Constraint(severity="error", key={l1, l2}, message="7 Lane") -pattern define_prevLane_lanecannotbeprevLaneof2lanes(l1:Lane, l2:Lane) { - Lane.prevLane(l1, l); - Lane.prevLane(l2, l); - l1 != l2; -} - -//////consecutive lanes must have same orientation -@Constraint(severity="error", key={l1, l2}, message="8 Lane") -pattern define_prevLane_consecutiveLanesMustHaveSameOrientation1(l1:Lane_Horizontal, l2:Lane_Vertical) { - Lane.prevLane(l1, l2); -} - -@Constraint(severity="error", key={l1, l2}, message="8 Lane") -pattern define_prevLane_consecutiveLanesMustHaveSameOrientation2(l1:Lane_Vertical, l2:Lane_Horizontal) { - Lane.prevLane(l1, l2); -} - -/////////////ReferenceCoord - -/////refCoord of head lanes must be 0 -@Constraint(severity="error", key={l}, message="6.2 Lane") -pattern define_prevLane_headHoriLaneHas0RefCoord(cs:CrossingScenario, l:Lane_Horizontal) { - CrossingScenario.horizontal_head(cs, l); - Lane.referenceCoord(l, rc); - check(rc != 0.0); -} - -@Constraint(severity="error", key={l}, message="6.2 Lane") -pattern define_prevLane_headVertLaneHas0RefCoord(cs:CrossingScenario, l:Lane_Vertical) { - CrossingScenario.vertical_head(cs, l); - Lane.referenceCoord(l, rc); - check(rc != 0.0); -} - -//////refCoord of a lane is prevLane.rc + curLane.numWidth - -@Constraint(severity="error", key={l}, message="6.2 Lane") -pattern define_referenceCoord_laneWithPrevHasCorrectRefCoord(l:Lane) { - Lane.prevLane(l, prev); - Lane.referenceCoord(l, rcCur); - - Lane.numWidth(prev, wPrev); - Lane.referenceCoord(prev, rcPrev); - check(rcCur != rcPrev + wPrev); -} - - -////////////// -//Lane+Actor -////////////// - -/////////Actor (a) on vertical lane (l) must have a.xPos=[l.rc, l.rc + l.nw] -@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") -pattern define_placedOn_actorOnVerticalLane(a : Actor, vl:Lane_Vertical) { - Actor.placedOn(a, vl); - Actor.xPos(a, x); - Lane.referenceCoord(vl, r); - check(x <= r); -} or { - Actor.placedOn(a, vl); - Actor.xPos(a, x); - Lane.referenceCoord(vl, r); - Lane.numWidth(vl, w); - check(x >= (r + w)); -} - -@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") -pattern define_placedOn_actorOnHorizLane(a : Actor, hl:Lane_Horizontal) { - Actor.placedOn(a, hl); - Actor.yPos(a, y); - Lane.referenceCoord(hl, r); - check(y <= r); -} or { - Actor.placedOn(a, hl); - Actor.yPos(a, y); - Lane.referenceCoord(hl, r); - Lane.numWidth(hl, w); - check(y >= (r + w)); -} - -////////////// -//Actor -////////////// - -////TODO -/////////xPos of every actor mmust be within bounds defined in CS -//@Constraint(severity="error", key={l}, message="1 Actor") -//pattern define_actor_xPosWithinCSbounds(cs:CrossingScenario, a:Actor) { -// -//} -// -////TODO -/////////yPos of every actor mmust be within bounds defined in CS -//@Constraint(severity="error", key={l}, message="2 Actor") -//pattern define_actor_yPosWithinCSbounds(cs:CrossingScenario, a:Actor) { -// -//} - - -/////////pedestrian-width (3) -pattern define_actor_pedestrianWidth(p:Pedestrian) { - Pedestrian.width(p, 1.0); -} - -/////////pedestrian-width (4) -pattern define_actor_pedestrianLength(p:Pedestrian) { - Pedestrian.length(p, 1.0); -} - -/////////actor-width (5) -pattern define_actor_actorWidth(a:Actor) { - Actor.placedOn(a, l); - Lane_Vertical(l); - Actor.width(p, 1.0); -} or { - Actor.placedOn(a, l); - Lane_Horizontal(l); - Actor.width(p, 3.0); -} - -/////////actor-width (6) -pattern define_actor_actorLength(a:Actor) { - Actor.placedOn(a, l); - Lane_Vertical(l); - Actor.length(p, 3.0); -} or { - Actor.placedOn(a, l); - Lane_Horizontal(l); - Actor.length(p, 1.0); -} - - -/////////xSpeed of actor on verticalLane is 0 -@Constraint(severity="error", key={a}, message="7 Actor") -pattern define_actor_actorOnVertLaneHasxSpeed0(a:Actor, vl:Lane_Vertical) { - Actor.placedOn(a, vl); - Actor.xSpeed(a, xSpeed); - check(xSpeed != 0); -} - -/////////ySpeed of actor on horizontalLane is 0 -@Constraint(severity="error", key={a}, message="8 Actor") -pattern define_actor_actorOnHoriLaneHasySpeed0(a:Actor, hl:Lane_Horizontal) { - Actor.placedOn(a, hl); - Actor.ySpeed(a, ySpeed); - check(ySpeed != 0); -} - -//////////////// -////CollisionExists -//////////////// -// -//@Constraint(severity="error", key={c}, message="x") -//pattern collisionExists_timeWithinBound(ss:CrossingScenario, c:CollisionExists) { -// CrossingScenario.actors.relations(ss, c); -// CrossingScenario.maxTime(ss, maxTime); -// CollisionExists. collisionTime(c, cTime); -// check(cTime >= maxTime);} -// -//@Constraint(severity="error", key={c}, message="x") -//pattern collisionExists_timeNotNegative(c:CollisionExists) { -// CollisionExists. collisionTime(c, cTime); -// check(cTime <= 0);} -// -//@Constraint(severity="error", key={a1, c}, message="x") -//pattern collisionExists_defineCollision_y1(a1:Actor, a2:Actor, c:CollisionExists) { -// Actor.relations(a1, c); -// CollisionExists.target(c, a2); -// -// Actor.length(a1, l1); -// Actor.yPos(a1, yPos1); -// Actor.ySpeed(a1, ySpeed1); -// Actor.length(a2, l2); -// Actor.yPos(a2, yPos2); -// Actor.ySpeed(a2, ySpeed2); -// CollisionExists. collisionTime(c, cTime); -// //check(y_1_bottom > y_2_top -// check((yPos1 + (ySpeed1 * cTime)) - (l1/2) > (yPos2 + (ySpeed2 * cTime)) + (l2/2)); -//} -// -//@Constraint(severity="error", key={a1, c}, message="x") -//pattern collisionExists_defineCollision_y2(a1:Actor, a2:Actor, c:CollisionExists) { -// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 -// Actor.relations(a1, c); -// CollisionExists.target(c, a2); -// -// Actor.length(a1, l1); -// Actor.yPos(a1, yPos1); -// Actor.ySpeed(a1, ySpeed1); -// Actor.length(a2, l2); -// Actor.yPos(a2, yPos2); -// Actor.ySpeed(a2, ySpeed2); -// CollisionExists. collisionTime(c, cTime); -// //check(y_1_top < y_2_bottom) -// check((yPos1 + (ySpeed1 * cTime)) + (l1/2) < (yPos2 + (ySpeed2 * cTime)) - (l2/2)); -//} -// -//@Constraint(severity="error", key={a1, c}, message="x") -//pattern collisionExists_defineCollision_x1(a1:Actor, a2:Actor, c:CollisionExists) { -// Actor.relations(a1, c); -// CollisionExists.target(c, a2); -// -// Actor.width(a1, w1); -// Actor.xPos(a1, xPos1); -// Actor.xSpeed(a1, xSpeed1); -// Actor.width(a2, w2); -// Actor.xPos(a2, xPos2); -// Actor.xSpeed(a2, xSpeed2); -// CollisionExists. collisionTime(c, cTime); -// //check(x_1_left > x_2_right) -// check((xPos1 + (xSpeed1 * cTime)) - (w1/2) > (xPos2 + (xSpeed2 * cTime)) + (w2/2)); -//} -// -//@Constraint(severity="error", key={a1, c}, message="x") -//pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor, c:CollisionExists) { -// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 -// Actor.relations(a1, c); -// CollisionExists.target(c, a2); -// -// Actor.width(a1, w1); -// Actor.xPos(a1, xPos1); -// Actor.xSpeed(a1, xSpeed1); -// Actor.width(a2, w2); -// Actor.xPos(a2, xPos2); -// Actor.xSpeed(a2, xSpeed2); -// CollisionExists. collisionTime(c, cTime); -// //check(x_1_right < x_2_left) -// check((xPos1 + (xSpeed1 * cTime)) + (w1/2) < (xPos2 + (xSpeed2 * cTime)) - (w2/2)); -//} -// -//////////////// -////SeparationDistance -//////////////// -//@Constraint(severity="error", key={a1, sd}, message="x") -//pattern SeparationDistance_near_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { -// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 -// Actor.relations(a1, sd); -// SeparationDistance.target(sd, a2); -// SeparationDistance.distance(sd, Distance::Near); -// -// Actor.xPos(a1, x1); -// Actor.yPos(a1, y1); -// Actor.xPos(a2, x2); -// Actor.yPos(a2, y2); -// //check(dx^2 + dy^2 < 5^2) -// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 5*5); -//} -// -//@Constraint(severity="error", key={a1, sd}, message="x") -//pattern SeparationDistance_near_ub(a1:Actor, a2:Actor, sd:SeparationDistance) { -// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 -// Actor.relations(a1, sd); -// SeparationDistance.target(sd, a2); -// SeparationDistance.distance(sd, Distance::Near); -// -// Actor.xPos(a1, x1); -// Actor.yPos(a1, y1); -// Actor.xPos(a2, x2); -// Actor.yPos(a2, y2); -// //check(dx^2 + dy^2 > 10^2) -// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10); -//} -// -//@Constraint(severity="error", key={a1, sd}, message="x") -//pattern SeparationDistance_medium_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { -// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 -// Actor.relations(a1, sd); -// SeparationDistance.target(sd, a2); -// SeparationDistance.distance(sd, Distance::Medium); -// -// Actor.xPos(a1, x1); -// Actor.yPos(a1, y1); -// Actor.xPos(a2, x2); -// Actor.yPos(a2, y2); -// //check(dx^2 + dy^2 < 10^2) -// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10); -//} -// -//@Constraint(severity="error", key={a1, sd}, message="x") -//pattern SeparationDistance_medium_ub(a1:Actor, a2:Actor, sd:SeparationDistance) { -// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 -// Actor.relations(a1, sd); -// SeparationDistance.target(sd, a2); -// SeparationDistance.distance(sd, Distance::Medium); -// -// Actor.xPos(a1, x1); -// Actor.yPos(a1, y1); -// Actor.xPos(a2, x2); -// Actor.yPos(a2, y2); -// //check(dx^2 + dy^2 > 1^2) -// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 15*15); -//} -// -//@Constraint(severity="error", key={a1, sd}, message="x") -//pattern SeparationDistance_far_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { -// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 -// Actor.relations(a1, sd); -// SeparationDistance.target(sd, a2); -// SeparationDistance.distance(sd, Distance::Far); -// -// Actor.xPos(a1, x1); -// Actor.yPos(a1, y1); -// Actor.xPos(a2, x2); -// Actor.yPos(a2, y2); -// //check(dx^2 + dy^2 < 15^2) -// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); -//} -// -//////////////// -////CollisionDoesNotExist -//////////////// -// -////@Constraint(severity="error", key={a1, cdne}, message="x") -////pattern collisionDoesNotExist(a1:Actor, a2:Actor, ss:CrossingScenario, cdne:CollisionDoesNotExist) { -//// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 -//// -//// CrossingScenario.actors(ss, a1); -//// CrossingScenario.actors(ss, a2); -//// Actor.relations(a1, cdne); -//// CollisionDoesNotExist.target(cdne, a2); -//// CrossingScenario.maxTime(ss, maxTime); -//// -//// Actor.width(a1, w1); -//// Actor.length(a1, l1); -//// Actor.xPos(a1, xPos1); -//// Actor.yPos(a1, yPos1); -//// Actor.xSpeed(a1, xSpeed1); -//// Actor.ySpeed(a1, ySpeed1); -//// -//// Actor.width(a2, w2); -//// Actor.length(a2, l2); -//// Actor.xPos(a2, xPos2); -//// Actor.yPos(a2, yPos2); -//// Actor.xSpeed(a2, xSpeed2); -//// Actor.ySpeed(a2, ySpeed2); -//// //check(dx^2 + dy^2 < 15^2) -//// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); -////} -// -//////////////// -////VisionBlocked -//////////////// -// -////OPTIONS 1: everything is from a single check expression containing ITEs -////Currently unhandled bygenerator -//@Constraint(severity="error", key={a1, vb}, message="x") -//pattern visionBlocked_ites_top(a1:Actor, a2:Actor, vb:VisionBlocked) { -// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 -// Actor.relations(a1, vb); -// VisionBlocked.target(vb, a2); -// VisionBlocked.blockedBy(vb, aBlocker); -// -// Actor.xPos(a1, x1); -// Actor.yPos(a1, y1); -// Actor.xPos(a2, x2); -// Actor.yPos(a2, y2); -// Actor.xPos(aBlocker, xBlocker); -// Actor.yPos(aBlocker, yBlocker); -// Actor.length(aBlocker, lenBlocker); -// Actor.width(aBlocker, widBlocker); -// -// //check(slope of a1-to-BlockerTop < slope of a1-to-a2) -// check( -// ( yBlocker - y1 + (if(xBlocker > x1){lenBlocker/2}else{0-lenBlocker/2})) / -// ( xBlocker - x1 + (if(yBlocker > y1){0-widBlocker/2}else{widBlocker/2})) -// < ((y1-y2)/(x1-x2))); -//} -// -//@Constraint(severity="error", key={a1, vb}, message="x") -//pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor, vb:VisionBlocked) { -// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 -// Actor.relations(a1, vb); -// VisionBlocked.target(vb, a2); -// VisionBlocked.blockedBy(vb, aBlocker); -// -// Actor.xPos(a1, x1); -// Actor.yPos(a1, y1); -// Actor.xPos(a2, x2); -// Actor.yPos(a2, y2); -// Actor.xPos(aBlocker, xBlocker); -// Actor.yPos(aBlocker, yBlocker); -// Actor.length(aBlocker, lenBlocker); -// Actor.width(aBlocker, widBlocker); -// -// //check(slope of a1-to-BlockerBottom > slope of a1-to-a2) -// check( -// ( yBlocker - y1 + (if(xBlocker > x1){0-lenBlocker/2}else{lenBlocker/2})) / -// ( xBlocker - x1 + (if(yBlocker > y1){widBlocker/2}else{0-widBlocker/2})) -// > ((y1-y2)/(x1-x2))); -//} -// -////OPTION 2: -////we handle ITE by seperating the constraints -// -////This will involve 1 constarint for each decision path, but will require multiple check expressions within the same pattern -// -////OPTION 3: -////If this is nott working still, we will have to add some strctural components to the MM -////to differentiate the different cases and reduce the requirements of if, then, else -// +package queries + +import "http://www.example.com/crossingScenario" +import "http://www.eclipse.org/emf/2002/Ecore" + +//////Minimal Failing Example +//@Constraint(severity = "error", key = {l}, message = "this defines the placedOn relation") +//pattern patterThatOnlyWorksWithInt(l : Lane) { +// Lane.referenceCoord(l, w); +// check(w <= 0-10.0); +//} + +////////////// +//CrossingScenario +///////////// + +//TODO Hard-code xSize? +//TODO Hard-code ySize? +//TODO Hard-code maxTime? + +////////////// +//Lane +////////////// + +@Constraint(severity="error", key={l}, message="1 Lane") +pattern define_numWidth_small(l : Lane) { + Lane.width(l, Size::S_Small); + Lane.numWidth(l, nw); + check(nw <= 5.0); +} or { + Lane.width(l, Size::S_Small); + Lane.numWidth(l, nw); + check(nw >= 10.0); +} + +@Constraint(severity="error", key={l}, message="2 Lane") +pattern define_numWidth_medium(l : Lane) { + Lane.width(l, ::S_Med); + Lane.numWidth(l, nw); + check(nw <= 10.0); +} +or { + Lane.width(l, Size::S_Med); + Lane.numWidth(l, nw); + check(nw >= 15.0); +} + +@Constraint(severity="error", key={l}, message="3 Lane") +pattern define_numWidth_large(l : Lane) { + Lane.width(l, Size::S_Large); + Lane.numWidth(l, nw); + check(nw <= 15.0); +} +or { + Lane.width(l, Size::S_Large); + Lane.numWidth(l, nw); + check(nw >= 20.0); +} + +/////////////Prevlane + +////////head lanes do not have prevLane +@Constraint(severity="error", key={l}, message="6.1 Lane") +pattern define_prevLane_headVertLaneDoesNotHavePrevLane(cs:CrossingScenario, l:Lane_Vertical) { + CrossingScenario.vertical_head(cs, l); + Lane.prevLane(l, _); +} + +@Constraint(severity="error", key={l}, message="6.2 Lane") +pattern define_prevLane_headHoriLaneDoesNotHavePrevLane(cs:CrossingScenario, l:Lane_Horizontal) { + CrossingScenario.horizontal_head(cs, l); + Lane.prevLane(l, _); +} + +////////Non-head lanes must have prevLane +@Constraint(severity="error", key={l}, message="6.1 Lane") +pattern define_prevLane_nonheadVertLaneHasPrevLane(l:Lane_Vertical) { + neg find find_headVertLane(l); + neg find find_laneWithPrevLane(l); +} + +@Constraint(severity="error", key={l}, message="6.1 Lane") +pattern define_prevLane_nonheadHoriLaneHasPrevLane(l:Lane_Horizontal) { + neg find find_headHoriLane(l); + neg find find_laneWithPrevLane(l); +} + +private pattern find_headVertLane(l:Lane_Vertical) { + CrossingScenario.vertical_head(_, l); +} +private pattern find_headHoriLane(l:Lane_Horizontal) { + CrossingScenario.horizontal_head(_, l); +} +private pattern find_laneWithPrevLane(l:Lane) { + Lane.prevLane(l, _); +} + +/////////Lane cannot be its own recursive prevLane +@Constraint(severity="error", key={l}, message="6.1 Lane") +pattern define_prevLane_lanecannotBeItsOwnPrevLane(l:Lane) { + Lane.prevLane(l, l); +} + +@Constraint(severity="error", key={l}, message="6.2 Lane") +pattern define_prevLane_lanecannotBeItsOwnRecursivePrevLane(l:Lane) { + find find_prevLane+(l, l); +} +private pattern find_prevLane(l1:Lane, l2:Lane) { + Lane.prevLane(l1, l2); +} + +//////Lane cannot be prevLane of >1 other lane +@Constraint(severity="error", key={l1, l2}, message="7 Lane") +pattern define_prevLane_lanecannotbeprevLaneof2lanes(l1:Lane, l2:Lane) { + Lane.prevLane(l1, l); + Lane.prevLane(l2, l); + l1 != l2; +} + +//////consecutive lanes must have same orientation +@Constraint(severity="error", key={l1, l2}, message="8 Lane") +pattern define_prevLane_consecutiveLanesMustHaveSameOrientation1(l1:Lane_Horizontal, l2:Lane_Vertical) { + Lane.prevLane(l1, l2); +} + +@Constraint(severity="error", key={l1, l2}, message="8 Lane") +pattern define_prevLane_consecutiveLanesMustHaveSameOrientation2(l1:Lane_Vertical, l2:Lane_Horizontal) { + Lane.prevLane(l1, l2); +} + +/////////////ReferenceCoord + +/////refCoord of head lanes must be 0 +@Constraint(severity="error", key={l}, message="6.2 Lane") +pattern define_prevLane_headHoriLaneHas0RefCoord(cs:CrossingScenario, l:Lane_Horizontal) { + CrossingScenario.horizontal_head(cs, l); + Lane.referenceCoord(l, rc); + check(rc != 0.0); +} + +@Constraint(severity="error", key={l}, message="6.2 Lane") +pattern define_prevLane_headVertLaneHas0RefCoord(cs:CrossingScenario, l:Lane_Vertical) { + CrossingScenario.vertical_head(cs, l); + Lane.referenceCoord(l, rc); + check(rc != 0.0); +} + +//////refCoord of a lane is prevLane.rc + curLane.numWidth + +@Constraint(severity="error", key={l}, message="6.2 Lane") +pattern define_referenceCoord_laneWithPrevHasCorrectRefCoord(l:Lane) { + Lane.prevLane(l, prev); + Lane.referenceCoord(l, rcCur); + + Lane.numWidth(prev, wPrev); + Lane.referenceCoord(prev, rcPrev); + check(rcCur != rcPrev + wPrev); +} + + +////////////// +//Lane+Actor +////////////// + +/////////Actor (a) on vertical lane (l) must have a.xPos=[l.rc, l.rc + l.nw] +@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") +pattern define_placedOn_actorOnVerticalLane(a : Actor, vl:Lane_Vertical) { + Actor.placedOn(a, vl); + Actor.xPos(a, x); + Lane.referenceCoord(vl, r); + check(x <= r); +} or { + Actor.placedOn(a, vl); + Actor.xPos(a, x); + Lane.referenceCoord(vl, r); + Lane.numWidth(vl, w); + check(x >= (r + w)); +} + +@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") +pattern define_placedOn_actorOnHorizLane(a : Actor, hl:Lane_Horizontal) { + Actor.placedOn(a, hl); + Actor.yPos(a, y); + Lane.referenceCoord(hl, r); + check(y <= r); +} or { + Actor.placedOn(a, hl); + Actor.yPos(a, y); + Lane.referenceCoord(hl, r); + Lane.numWidth(hl, w); + check(y >= (r + w)); +} + +////////////// +//Actor +////////////// + +////TODO +/////////xPos of every actor mmust be within bounds defined in CS +//@Constraint(severity="error", key={l}, message="1 Actor") +//pattern define_actor_xPosWithinCSbounds(cs:CrossingScenario, a:Actor) { +// +//} +// +////TODO +/////////yPos of every actor mmust be within bounds defined in CS +//@Constraint(severity="error", key={l}, message="2 Actor") +//pattern define_actor_yPosWithinCSbounds(cs:CrossingScenario, a:Actor) { +// +//} + + +/////////pedestrian-width (3) +//pattern define_actor_pedestrianWidth(p:Pedestrian) { +// Pedestrian.width(p, 1.0); +//} +// +///////////pedestrian-width (4) +//pattern define_actor_pedestrianLength(p:Pedestrian) { +// Pedestrian.length(p, 1.0); +//} + +///////////actor-width (5) +//pattern define_actor_actorWidth(a:Actor) { +// Actor.placedOn(a, l); +// Lane_Vertical(l); +// Actor.width(p, 1.0); +//} or { +// Actor.placedOn(a, l); +// Lane_Horizontal(l); +// Actor.width(p, 3.0); +//} +// +///////////actor-width (6) +//pattern define_actor_actorLength(a:Actor) { +// Actor.placedOn(a, l); +// Lane_Vertical(l); +// Actor.length(p, 3.0); +//} or { +// Actor.placedOn(a, l); +// Lane_Horizontal(l); +// Actor.length(p, 1.0); +//} + + +/////////xSpeed of actor on verticalLane is 0 +@Constraint(severity="error", key={a}, message="7 Actor") +pattern define_actor_actorOnVertLaneHasxSpeed0(a:Actor, vl:Lane_Vertical) { + Actor.placedOn(a, vl); + Actor.xSpeed(a, xSpeed); + check(xSpeed != 0); +} + +/////////ySpeed of actor on horizontalLane is 0 +@Constraint(severity="error", key={a}, message="8 Actor") +pattern define_actor_actorOnHoriLaneHasySpeed0(a:Actor, hl:Lane_Horizontal) { + Actor.placedOn(a, hl); + Actor.ySpeed(a, ySpeed); + check(ySpeed != 0); +} + +//////////////// +////CollisionExists +//////////////// +// +//@Constraint(severity="error", key={c}, message="x") +//pattern collisionExists_timeWithinBound(ss:CrossingScenario, c:CollisionExists) { +// CrossingScenario.actors.relations(ss, c); +// CrossingScenario.maxTime(ss, maxTime); +// CollisionExists. collisionTime(c, cTime); +// check(cTime >= maxTime);} +// +//@Constraint(severity="error", key={c}, message="x") +//pattern collisionExists_timeNotNegative(c:CollisionExists) { +// CollisionExists. collisionTime(c, cTime); +// check(cTime <= 0);} +// +//@Constraint(severity="error", key={a1, c}, message="x") +//pattern collisionExists_defineCollision_y1(a1:Actor, a2:Actor, c:CollisionExists) { +// Actor.relations(a1, c); +// CollisionExists.target(c, a2); +// +// Actor.length(a1, l1); +// Actor.yPos(a1, yPos1); +// Actor.ySpeed(a1, ySpeed1); +// Actor.length(a2, l2); +// Actor.yPos(a2, yPos2); +// Actor.ySpeed(a2, ySpeed2); +// CollisionExists. collisionTime(c, cTime); +// //check(y_1_bottom > y_2_top +// check((yPos1 + (ySpeed1 * cTime)) - (l1/2) > (yPos2 + (ySpeed2 * cTime)) + (l2/2)); +//} +// +//@Constraint(severity="error", key={a1, c}, message="x") +//pattern collisionExists_defineCollision_y2(a1:Actor, a2:Actor, c:CollisionExists) { +// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 +// Actor.relations(a1, c); +// CollisionExists.target(c, a2); +// +// Actor.length(a1, l1); +// Actor.yPos(a1, yPos1); +// Actor.ySpeed(a1, ySpeed1); +// Actor.length(a2, l2); +// Actor.yPos(a2, yPos2); +// Actor.ySpeed(a2, ySpeed2); +// CollisionExists. collisionTime(c, cTime); +// //check(y_1_top < y_2_bottom) +// check((yPos1 + (ySpeed1 * cTime)) + (l1/2) < (yPos2 + (ySpeed2 * cTime)) - (l2/2)); +//} +// +//@Constraint(severity="error", key={a1, c}, message="x") +//pattern collisionExists_defineCollision_x1(a1:Actor, a2:Actor, c:CollisionExists) { +// Actor.relations(a1, c); +// CollisionExists.target(c, a2); +// +// Actor.width(a1, w1); +// Actor.xPos(a1, xPos1); +// Actor.xSpeed(a1, xSpeed1); +// Actor.width(a2, w2); +// Actor.xPos(a2, xPos2); +// Actor.xSpeed(a2, xSpeed2); +// CollisionExists. collisionTime(c, cTime); +// //check(x_1_left > x_2_right) +// check((xPos1 + (xSpeed1 * cTime)) - (w1/2) > (xPos2 + (xSpeed2 * cTime)) + (w2/2)); +//} +// +//@Constraint(severity="error", key={a1, c}, message="x") +//pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor, c:CollisionExists) { +// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 +// Actor.relations(a1, c); +// CollisionExists.target(c, a2); +// +// Actor.width(a1, w1); +// Actor.xPos(a1, xPos1); +// Actor.xSpeed(a1, xSpeed1); +// Actor.width(a2, w2); +// Actor.xPos(a2, xPos2); +// Actor.xSpeed(a2, xSpeed2); +// CollisionExists. collisionTime(c, cTime); +// //check(x_1_right < x_2_left) +// check((xPos1 + (xSpeed1 * cTime)) + (w1/2) < (xPos2 + (xSpeed2 * cTime)) - (w2/2)); +//} +// +//////////////// +////SeparationDistance +//////////////// +//@Constraint(severity="error", key={a1, sd}, message="x") +//pattern SeparationDistance_near_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { +// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 +// Actor.relations(a1, sd); +// SeparationDistance.target(sd, a2); +// SeparationDistance.distance(sd, Distance::Near); +// +// Actor.xPos(a1, x1); +// Actor.yPos(a1, y1); +// Actor.xPos(a2, x2); +// Actor.yPos(a2, y2); +// //check(dx^2 + dy^2 < 5^2) +// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 5*5); +//} +// +//@Constraint(severity="error", key={a1, sd}, message="x") +//pattern SeparationDistance_near_ub(a1:Actor, a2:Actor, sd:SeparationDistance) { +// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 +// Actor.relations(a1, sd); +// SeparationDistance.target(sd, a2); +// SeparationDistance.distance(sd, Distance::Near); +// +// Actor.xPos(a1, x1); +// Actor.yPos(a1, y1); +// Actor.xPos(a2, x2); +// Actor.yPos(a2, y2); +// //check(dx^2 + dy^2 > 10^2) +// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10); +//} +// +//@Constraint(severity="error", key={a1, sd}, message="x") +//pattern SeparationDistance_medium_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { +// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 +// Actor.relations(a1, sd); +// SeparationDistance.target(sd, a2); +// SeparationDistance.distance(sd, Distance::Medium); +// +// Actor.xPos(a1, x1); +// Actor.yPos(a1, y1); +// Actor.xPos(a2, x2); +// Actor.yPos(a2, y2); +// //check(dx^2 + dy^2 < 10^2) +// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10); +//} +// +//@Constraint(severity="error", key={a1, sd}, message="x") +//pattern SeparationDistance_medium_ub(a1:Actor, a2:Actor, sd:SeparationDistance) { +// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 +// Actor.relations(a1, sd); +// SeparationDistance.target(sd, a2); +// SeparationDistance.distance(sd, Distance::Medium); +// +// Actor.xPos(a1, x1); +// Actor.yPos(a1, y1); +// Actor.xPos(a2, x2); +// Actor.yPos(a2, y2); +// //check(dx^2 + dy^2 > 1^2) +// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 15*15); +//} +// +//@Constraint(severity="error", key={a1, sd}, message="x") +//pattern SeparationDistance_far_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { +// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 +// Actor.relations(a1, sd); +// SeparationDistance.target(sd, a2); +// SeparationDistance.distance(sd, Distance::Far); +// +// Actor.xPos(a1, x1); +// Actor.yPos(a1, y1); +// Actor.xPos(a2, x2); +// Actor.yPos(a2, y2); +// //check(dx^2 + dy^2 < 15^2) +// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); +//} +// +//////////////// +////CollisionDoesNotExist +//////////////// +// +////@Constraint(severity="error", key={a1, cdne}, message="x") +////pattern collisionDoesNotExist(a1:Actor, a2:Actor, ss:CrossingScenario, cdne:CollisionDoesNotExist) { +//// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 +//// +//// CrossingScenario.actors(ss, a1); +//// CrossingScenario.actors(ss, a2); +//// Actor.relations(a1, cdne); +//// CollisionDoesNotExist.target(cdne, a2); +//// CrossingScenario.maxTime(ss, maxTime); +//// +//// Actor.width(a1, w1); +//// Actor.length(a1, l1); +//// Actor.xPos(a1, xPos1); +//// Actor.yPos(a1, yPos1); +//// Actor.xSpeed(a1, xSpeed1); +//// Actor.ySpeed(a1, ySpeed1); +//// +//// Actor.width(a2, w2); +//// Actor.length(a2, l2); +//// Actor.xPos(a2, xPos2); +//// Actor.yPos(a2, yPos2); +//// Actor.xSpeed(a2, xSpeed2); +//// Actor.ySpeed(a2, ySpeed2); +//// //check(dx^2 + dy^2 < 15^2) +//// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); +////} +// +//////////////// +////VisionBlocked +//////////////// +// +////OPTIONS 1: everything is from a single check expression containing ITEs +////Currently unhandled bygenerator +//@Constraint(severity="error", key={a1, vb}, message="x") +//pattern visionBlocked_ites_top(a1:Actor, a2:Actor, vb:VisionBlocked) { +// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 +// Actor.relations(a1, vb); +// VisionBlocked.target(vb, a2); +// VisionBlocked.blockedBy(vb, aBlocker); +// +// Actor.xPos(a1, x1); +// Actor.yPos(a1, y1); +// Actor.xPos(a2, x2); +// Actor.yPos(a2, y2); +// Actor.xPos(aBlocker, xBlocker); +// Actor.yPos(aBlocker, yBlocker); +// Actor.length(aBlocker, lenBlocker); +// Actor.width(aBlocker, widBlocker); +// +// //check(slope of a1-to-BlockerTop < slope of a1-to-a2) +// check( +// ( yBlocker - y1 + (if(xBlocker > x1){lenBlocker/2}else{0-lenBlocker/2})) / +// ( xBlocker - x1 + (if(yBlocker > y1){0-widBlocker/2}else{widBlocker/2})) +// < ((y1-y2)/(x1-x2))); +//} +// +//@Constraint(severity="error", key={a1, vb}, message="x") +//pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor, vb:VisionBlocked) { +// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 +// Actor.relations(a1, vb); +// VisionBlocked.target(vb, a2); +// VisionBlocked.blockedBy(vb, aBlocker); +// +// Actor.xPos(a1, x1); +// Actor.yPos(a1, y1); +// Actor.xPos(a2, x2); +// Actor.yPos(a2, y2); +// Actor.xPos(aBlocker, xBlocker); +// Actor.yPos(aBlocker, yBlocker); +// Actor.length(aBlocker, lenBlocker); +// Actor.width(aBlocker, widBlocker); +// +// //check(slope of a1-to-BlockerBottom > slope of a1-to-a2) +// check( +// ( yBlocker - y1 + (if(xBlocker > x1){0-lenBlocker/2}else{lenBlocker/2})) / +// ( xBlocker - x1 + (if(yBlocker > y1){widBlocker/2}else{0-widBlocker/2})) +// > ((y1-y2)/(x1-x2))); +//} +// +////OPTION 2: +////we handle ITE by seperating the constraints +// +////This will involve 1 constarint for each decision path, but will require multiple check expressions within the same pattern +// +////OPTION 3: +////If this is nott working still, we will have to add some strctural components to the MM +////to differentiate the different cases and reduce the requirements of if, then, else +// ////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 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - +--> + + + + + + + + + + + + + + + + + + + + + + + + + + + + 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 @@ - - - - - - - - - - - - - - - - - - - - - - - - - +--> + + + + + + + + + + + + + + + + + + + + + + + + + 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; import java.io.IOException; import java.io.InputStream; import java.io.InputStreamReader; +import java.io.PrintWriter; import java.util.ArrayList; import java.util.Arrays; import java.util.HashMap; @@ -28,43 +29,53 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement; public class NumericDrealProblemSolver extends NumericProblemSolver{ + + private final boolean useDocker; - private final String containerName; + private String containerName = ""; + private String drealLocalPath = ""; private final String smtFileName = "tmp/smt.smt2"; private Map varMap; private Map curVar2Decl; + + private final int TIMEOUT_DOCKER = 5; + private final int TIMEOUT_LOCAL = 2; - public NumericDrealProblemSolver() throws IOException, InterruptedException { + public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath) throws IOException, InterruptedException { + this.useDocker = useDocker; + this.varMap = new HashMap(); + this.drealLocalPath = drealLocalPath; + + if (useDocker) setupDocker(); + } + + private void setupDocker() throws IOException, InterruptedException { //setup docker //TODO ENSURE that container name is not already in use???? //TODO if dreal/dreal4 image is not downloaded, download it. - File tempDir = new File(System.getProperty("java.io.tmpdir")); - containerName = UUID.randomUUID().toString().replace("-", ""); + this.containerName = UUID.randomUUID().toString().replace("-", ""); List startDocker = new ArrayList( Arrays.asList("docker", "run", "-id", "--rm", "--name", containerName, // "-p", "8080:80", "dreal/dreal4")); - runProcess(startDocker); - - //setup varmap - varMap = new HashMap(); + runProcess(startDocker, TIMEOUT_DOCKER); } - private Process runProcess(List cmd) throws IOException, InterruptedException { + private Process runProcess(List cmd, int timeout) throws IOException, InterruptedException { String s = String.join(" ", cmd); Process p = Runtime.getRuntime().exec(s); // p.waitFor(); //TODO timeout if needed - if (!p.waitFor(5, TimeUnit.SECONDS)) { + if (!p.waitFor(timeout, TimeUnit.SECONDS)) { p.destroy(); System.err.println("TIMEOUT"); //DEBUG } return p; } - private Process callDreal(List numProbContents, boolean getModel) throws IOException, InterruptedException { + private Process callDrealDocker(List numProbContents, boolean getModel) throws IOException, InterruptedException { String numProbContentStr = String.join("\\n", numProbContents); List drealCmd = new ArrayList(Arrays.asList( "docker", "exec", containerName, @@ -78,7 +89,28 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ if (getModel) {drealCmd.add("--model");} drealCmd.add(smtFileName + "\""); - return runProcess(drealCmd); + return runProcess(drealCmd, TIMEOUT_DOCKER); + } + + private Process callDrealLocal(List numProbContents, boolean getModel) throws IOException, InterruptedException { + //print numProbConents to temp file + File tempFile = File.createTempFile("smt", ".smt2"); + + PrintWriter printer = new PrintWriter(tempFile); + for (String s : numProbContents) { + printer.println(s); + } + printer.close(); + + //call local dreal with path to temp file + List drealCmd = new ArrayList(); + drealCmd.add(drealLocalPath); + if (getModel) {drealCmd.add("--model");} + drealCmd.add(tempFile.getAbsolutePath()); + + System.out.println(drealCmd); + + return runProcess(drealCmd, TIMEOUT_LOCAL); } private List getDrealStream(InputStream stream) throws IOException { @@ -262,6 +294,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ } } + @SuppressWarnings("unused") private void printOutput(List list) { for (String line : list) { System.out.println(line); @@ -282,7 +315,11 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ //CALL DREAL long startSolvingProblem = System.nanoTime(); - Process outputProcess = callDreal(numProbContent, false); + + Process outputProcess; + if (this.useDocker) outputProcess = callDrealDocker(numProbContent, false); + else outputProcess = callDrealLocal(numProbContent, false); + List> outputs = getProcessOutput(outputProcess); boolean result = getDrealResult(outputProcess.exitValue(), outputs); endSolvingProblem = System.nanoTime()-startSolvingProblem; @@ -320,10 +357,15 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ long startformingProblem = System.nanoTime(); List numProbContent = formNumericProblemInstance(matches); endformingProblem = System.nanoTime()-startformingProblem; - + + //CALL DREAL long startSolvingProblem = System.nanoTime(); - Process outputProcess = callDreal(numProbContent, true); + + Process outputProcess; + if (this.useDocker) outputProcess = callDrealDocker(numProbContent, false); + else outputProcess = callDrealLocal(numProbContent, false); + List> outputs = getProcessOutput(outputProcess); boolean result = getDrealResult(outputProcess.exitValue(), outputs); endSolvingProblem = System.nanoTime()-startSolvingProblem; @@ -373,7 +415,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ public void teardown() throws IOException, InterruptedException { List stopDocker = new ArrayList( Arrays.asList("docker", "stop", containerName)); - runProcess(stopDocker); + runProcess(stopDocker, TIMEOUT_DOCKER); //TODO Check if above went well? } 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 @@ - - - - - - - - - - - - - - + + + + + + + + + + + + + + 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 { val solverTime = System.nanoTime - solverStartTime viatraConfig.progressMonitor.workedSearchFinished - //dreal teardown - if (viatraConfig.numericSolverSelection == NumericSolverSelection.DREAL){ + //dreal docker teardown + if (viatraConfig.numericSolverSelection == NumericSolverSelection.DREAL_DOCKER){ (numericSolver.numericSolverSelection as NumericDrealProblemSolver).teardown() } 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 { } enum NumericSolverSelection { - DREAL, + DREAL_DOCKER, + DREAL_LOCAL, Z3 } @@ -75,7 +76,8 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration { public var nonContainmentWeight = 1 public var unfinishedWFWeight = 1 public var calculateObjectCreationCosts = false - public var numericSolverSelection = NumericSolverSelection.DREAL //currently defaulted to DREAL + public var numericSolverSelection = NumericSolverSelection.DREAL_DOCKER //currently defaulted to DREAL + public var drealLocalPath = ""; public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral( 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 { val boolean intermediateConsistencyCheck val boolean caching; Map>>,Boolean> satisfiabilityCache = new HashMap + val String drealLocalPath; var long runtime = 0 var long cachingTime = 0 @@ -43,12 +44,16 @@ class NumericSolver { new(ModelGenerationMethod method, ViatraReasonerConfiguration config, boolean caching) { this.method = method this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks - this.t = new NumericTranslator(createNumericTranslator(config.numericSolverSelection)) this.caching = caching + this.drealLocalPath = config.drealLocalPath + this.t = new NumericTranslator(createNumericTranslator(config.numericSolverSelection)) } def createNumericTranslator(NumericSolverSelection solverSelection) { - if (solverSelection == NumericSolverSelection.DREAL) return new NumericDrealProblemSolver + if (solverSelection == NumericSolverSelection.DREAL_DOCKER) + return new NumericDrealProblemSolver(true, null) + if (solverSelection == NumericSolverSelection.DREAL_LOCAL) + return new NumericDrealProblemSolver(false, drealLocalPath) if (solverSelection == NumericSolverSelection.Z3) return new NumericZ3ProblemSolver } @@ -98,12 +103,12 @@ class NumericSolver { finalResult=true } else { val propagatedConstraints = new HashMap - println("------ Any matches?") + println("<<<>>>") for(entry : matches.entrySet) { val constraint = entry.key - println("------ " + constraint) +// println("--match?-- " + constraint) val allMatches = entry.value.allMatches.map[it.toArray] - println("------ " + allMatches.toList) +// println("---------- " + entry.value.allMatches) propagatedConstraints.put(constraint,allMatches) } if(propagatedConstraints.values.forall[empty]) { -- cgit v1.2.3-54-g00ecf