diff options
author | 2021-01-19 12:46:58 +0100 | |
---|---|---|
committer | 2021-01-19 12:46:58 +0100 | |
commit | 953227f62ece22f06bc54a47eeec8bf79b25dc27 (patch) | |
tree | 72bf39c26b2e58bd5ac4ba0506cf78608e80c309 /Domains/crossingScenario/src | |
parent | add vsconfig flag to allow running dreal locally (diff) | |
download | VIATRA-Generator-953227f62ece22f06bc54a47eeec8bf79b25dc27.tar.gz VIATRA-Generator-953227f62ece22f06bc54a47eeec8bf79b25dc27.tar.zst VIATRA-Generator-953227f62ece22f06bc54a47eeec8bf79b25dc27.zip |
add Actor+CollisionExists constrs & adjust dreal parser & measurements
Diffstat (limited to 'Domains/crossingScenario/src')
-rw-r--r-- | Domains/crossingScenario/src/crossingScenario/run/CrossingScenarioMain.java | 17 | ||||
-rw-r--r-- | Domains/crossingScenario/src/crossingScenario/run/QueryDebug.java | 23 |
2 files changed, 26 insertions, 14 deletions
diff --git a/Domains/crossingScenario/src/crossingScenario/run/CrossingScenarioMain.java b/Domains/crossingScenario/src/crossingScenario/run/CrossingScenarioMain.java index c0646edd..9b8f10dc 100644 --- a/Domains/crossingScenario/src/crossingScenario/run/CrossingScenarioMain.java +++ b/Domains/crossingScenario/src/crossingScenario/run/CrossingScenarioMain.java | |||
@@ -15,7 +15,13 @@ public class CrossingScenarioMain { | |||
15 | throw new IllegalStateException("This is a static utility class and should not be instantiated directly."); | 15 | throw new IllegalStateException("This is a static utility class and should not be instantiated directly."); |
16 | } | 16 | } |
17 | 17 | ||
18 | public static void main(String[] args) throws IOException { | 18 | public static void main(String[] args) throws IOException, InterruptedException { |
19 | // System.out.println(System.getProperty("java.library.path")); | ||
20 | //// System.setProperty("java.library.path", | ||
21 | //// "/home/models/VIATRA-Generator/Solvers/SMT-Solver/com.microsoft.z3/lib"); | ||
22 | // Thread.sleep(2000); | ||
23 | // System.out.println(System.getProperty("java.library.path")); | ||
24 | // System.loadLibrary("z3java"); | ||
19 | String errorMessages = StandaloneScriptExecutor.executeScript("inputs/crossingScenarioGen.vsconfig"); | 25 | String errorMessages = StandaloneScriptExecutor.executeScript("inputs/crossingScenarioGen.vsconfig"); |
20 | if (errorMessages != null) { | 26 | if (errorMessages != null) { |
21 | System.out.println(errorMessages); | 27 | System.out.println(errorMessages); |
@@ -28,10 +34,11 @@ public class CrossingScenarioMain { | |||
28 | int t2 = Integer.parseInt(times[4]); | 34 | int t2 = Integer.parseInt(times[4]); |
29 | int t3 = Integer.parseInt(times[5]); | 35 | int t3 = Integer.parseInt(times[5]); |
30 | int t4 = Integer.parseInt(times[6]); | 36 | int t4 = Integer.parseInt(times[6]); |
37 | int t5 = Integer.parseInt(times[7]); | ||
31 | int tot = t1+t2+t3+t4; | 38 | int tot = t1+t2+t3+t4; |
32 | System.out.println("domain2logic -> " + t1); | 39 | System.out.println("preprocessingTime -> ~" + (t1+t2)); |
33 | System.out.println("logic2solver -> " + t2); | 40 | System.out.println("sol0FoundAt -> " + (t5)); |
34 | System.out.println("solver -> " + t3); | 41 | System.out.println("solver -> ~" + t3); |
35 | System.out.println("postprocessing -> " + t4); | 42 | System.out.println("postprocessing -> " + t4); |
36 | 43 | ||
37 | System.out.println("TOTAL -> " + tot); | 44 | System.out.println("TOTAL -> " + tot); |
@@ -39,6 +46,6 @@ public class CrossingScenarioMain { | |||
39 | String p1 = "outputs/models/1.xmi"; | 46 | String p1 = "outputs/models/1.xmi"; |
40 | String p2 = "outputs/simplePrevLane.tgf"; | 47 | String p2 = "outputs/simplePrevLane.tgf"; |
41 | QueryDebug.checkPrevLanes(p1, p2); | 48 | QueryDebug.checkPrevLanes(p1, p2); |
42 | Desktop.getDesktop().open(new File(p2)); | 49 | // Desktop.getDesktop().open(new File(p2)); |
43 | } | 50 | } |
44 | } | 51 | } |
diff --git a/Domains/crossingScenario/src/crossingScenario/run/QueryDebug.java b/Domains/crossingScenario/src/crossingScenario/run/QueryDebug.java index 51ace4b8..f9041e87 100644 --- a/Domains/crossingScenario/src/crossingScenario/run/QueryDebug.java +++ b/Domains/crossingScenario/src/crossingScenario/run/QueryDebug.java | |||
@@ -23,11 +23,16 @@ import crossingScenario.Lane; | |||
23 | 23 | ||
24 | public class QueryDebug { | 24 | public class QueryDebug { |
25 | public static void main(String[] args) throws FileNotFoundException { | 25 | public static void main(String[] args) throws FileNotFoundException { |
26 | checkPrevLanes("outputs/models/1.xmi", "outputs/simplePrevLane.tgf"); | 26 | // checkPrevLanes("outputs/models/1.xmi", "outputs/simplePrevLane.tgf"); |
27 | // testOnInstance(); | 27 | testOnInstance(); |
28 | // miniRETest("21/2"); | 28 | // miniRETest("21/2"); |
29 | } | 29 | } |
30 | 30 | ||
31 | private static Double rndbl(Double in, int places) { | ||
32 | double scale = Math.pow(10, places); | ||
33 | return Math.round(in * scale) / scale; | ||
34 | } | ||
35 | |||
31 | public static void checkPrevLanes(String pathSrc, String pathTgt) throws FileNotFoundException { | 36 | public static void checkPrevLanes(String pathSrc, String pathTgt) throws FileNotFoundException { |
32 | Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap( ).put("*", new XMIResourceFactoryImpl()); | 37 | Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap( ).put("*", new XMIResourceFactoryImpl()); |
33 | EPackage.Registry.INSTANCE.put(CrossingScenarioPackage.eNS_URI, CrossingScenarioPackage.eINSTANCE); | 38 | EPackage.Registry.INSTANCE.put(CrossingScenarioPackage.eNS_URI, CrossingScenarioPackage.eINSTANCE); |
@@ -39,7 +44,7 @@ public class QueryDebug { | |||
39 | CrossingScenario cs = ((CrossingScenario) res.getContents().get(0)); | 44 | CrossingScenario cs = ((CrossingScenario) res.getContents().get(0)); |
40 | 45 | ||
41 | for (Actor o : cs.getActors()) { | 46 | for (Actor o : cs.getActors()) { |
42 | String nodeName = "(" + o.getXPos()+","+o.getYPos() + ")"; | 47 | String nodeName = "A(" + rndbl(o.getXPos(), 1)+","+rndbl(o.getYPos(), 1) + ")"; |
43 | printer.println(o.hashCode() + " " + nodeName); | 48 | printer.println(o.hashCode() + " " + nodeName); |
44 | } | 49 | } |
45 | 50 | ||
@@ -48,7 +53,7 @@ public class QueryDebug { | |||
48 | if (cs.getHorizontal_head().equals(o) || cs.getVertical_head().equals(o)) { | 53 | if (cs.getHorizontal_head().equals(o) || cs.getVertical_head().equals(o)) { |
49 | prefix = "HEAD"; | 54 | prefix = "HEAD"; |
50 | } | 55 | } |
51 | String nodeName = prefix + "(" + o.getReferenceCoord() + ")" + | 56 | String nodeName = prefix + "L(" + rndbl(o.getReferenceCoord(), 3) + ")" + |
52 | o.eClass().getName().substring(5, 9); | 57 | o.eClass().getName().substring(5, 9); |
53 | printer.println(o.hashCode() + " " + nodeName); | 58 | printer.println(o.hashCode() + " " + nodeName); |
54 | } | 59 | } |
@@ -57,7 +62,7 @@ public class QueryDebug { | |||
57 | if (o.getPrevLane() != null){ | 62 | if (o.getPrevLane() != null){ |
58 | int curName = o.hashCode(); | 63 | int curName = o.hashCode(); |
59 | int curPrev = o.getPrevLane().hashCode(); | 64 | int curPrev = o.getPrevLane().hashCode(); |
60 | double edgeLabel = o.getPrevLane().getNumWidth(); | 65 | double edgeLabel = rndbl(o.getPrevLane().getNumWidth(), 1); |
61 | printer.println(curName + " " + curPrev + " " + edgeLabel); | 66 | printer.println(curName + " " + curPrev + " " + edgeLabel); |
62 | } | 67 | } |
63 | } | 68 | } |
@@ -82,14 +87,14 @@ public class QueryDebug { | |||
82 | 87 | ||
83 | // ViatraQueryEngine engine = ViatraQueryEngine.on(new EMFScope(rs)); | 88 | // ViatraQueryEngine engine = ViatraQueryEngine.on(new EMFScope(rs)); |
84 | // // Access pattern matcher | 89 | // // Access pattern matcher |
85 | // CrossingScenarioQueries.instance().prepare(engine); | 90 | // Queries.instance().prepare(engine); |
86 | // | 91 | // |
87 | // Define_referenceCoord_laneWithPrevHasCorrectRefCoord.Matcher matcher = Define_referenceCoord_laneWithPrevHasCorrectRefCoord.Matcher.on(engine); | 92 | // X.Matcher matcher = X.Matcher.on(engine); |
88 | // // Get and iterate over all matches | 93 | // // Get and iterate over all matches |
89 | // System.out.println("MATCHES:"); | 94 | // System.out.println("MATCHES:"); |
90 | // for (Define_referenceCoord_laneWithPrevHasCorrectRefCoord.Match match : matcher.getAllMatches()) { | 95 | // for (X.Match match : matcher.getAllMatches()) { |
91 | // // Print all the matches to the standard output | 96 | // // Print all the matches to the standard output |
92 | // System.out.println(match.getL()); | 97 | // System.out.println(match.getP()); |
93 | // } | 98 | // } |
94 | } | 99 | } |
95 | 100 | ||