From 953227f62ece22f06bc54a47eeec8bf79b25dc27 Mon Sep 17 00:00:00 2001
From: Aren Babikian <aren.babikian@mail.mcgill.ca>
Date: Tue, 19 Jan 2021 12:46:58 +0100
Subject: add Actor+CollisionExists constrs & adjust dreal parser &
 measurements

---
 .../crossingScenario/run/CrossingScenarioMain.java | 17 +++++++++++-----
 .../src/crossingScenario/run/QueryDebug.java       | 23 +++++++++++++---------
 2 files changed, 26 insertions(+), 14 deletions(-)

(limited to 'Domains/crossingScenario/src')

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 {
 		throw new IllegalStateException("This is a static utility class and should not be instantiated directly.");
 	}
 
-	public static void main(String[] args) throws IOException {
+	public static void main(String[] args) throws IOException, InterruptedException {
+//		System.out.println(System.getProperty("java.library.path"));
+////		System.setProperty("java.library.path", 
+////				"/home/models/VIATRA-Generator/Solvers/SMT-Solver/com.microsoft.z3/lib");
+//		Thread.sleep(2000);
+//		System.out.println(System.getProperty("java.library.path"));
+//		System.loadLibrary("z3java");
 		String errorMessages = StandaloneScriptExecutor.executeScript("inputs/crossingScenarioGen.vsconfig");
 		if (errorMessages != null) {
 			System.out.println(errorMessages);
@@ -28,10 +34,11 @@ public class CrossingScenarioMain {
 		int t2 = Integer.parseInt(times[4]);
 		int t3 = Integer.parseInt(times[5]);
 		int t4 = Integer.parseInt(times[6]);
+		int t5 = Integer.parseInt(times[7]);
 		int tot = t1+t2+t3+t4;
-		System.out.println("domain2logic -> " + t1);
-		System.out.println("logic2solver -> " + t2);
-		System.out.println("solver -> " + t3);
+		System.out.println("preprocessingTime -> ~" + (t1+t2));
+		System.out.println("sol0FoundAt -> " + (t5));
+		System.out.println("solver -> ~" + t3);
 		System.out.println("postprocessing -> " + t4);
 		
 		System.out.println("TOTAL -> " + tot);
@@ -39,6 +46,6 @@ public class CrossingScenarioMain {
 		String p1 = "outputs/models/1.xmi";
 		String p2 = "outputs/simplePrevLane.tgf";
 		QueryDebug.checkPrevLanes(p1, p2);
-		Desktop.getDesktop().open(new File(p2));  
+//		Desktop.getDesktop().open(new File(p2));  
 	}
 }
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;
 
 public class QueryDebug {
 	public static void main(String[] args) throws FileNotFoundException {
-		checkPrevLanes("outputs/models/1.xmi", "outputs/simplePrevLane.tgf");
-//		testOnInstance();
+//		checkPrevLanes("outputs/models/1.xmi", "outputs/simplePrevLane.tgf");
+		testOnInstance();
 //		miniRETest("21/2");
 	}
 	
+	private static Double rndbl(Double in, int places) {
+	    double scale = Math.pow(10, places);
+	    return Math.round(in * scale) / scale;		
+	}
+	
 	public static void checkPrevLanes(String pathSrc, String pathTgt) throws FileNotFoundException {
 		Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap( ).put("*", new XMIResourceFactoryImpl());
 		EPackage.Registry.INSTANCE.put(CrossingScenarioPackage.eNS_URI, CrossingScenarioPackage.eINSTANCE);
@@ -39,7 +44,7 @@ public class QueryDebug {
 		CrossingScenario cs = ((CrossingScenario) res.getContents().get(0));
 		
 		for (Actor o : cs.getActors()) {
-			String nodeName = "(" + o.getXPos()+","+o.getYPos() + ")";
+			String nodeName = "A(" + rndbl(o.getXPos(), 1)+","+rndbl(o.getYPos(), 1) + ")";
 			printer.println(o.hashCode() + " " + nodeName);
 		}
 		
@@ -48,7 +53,7 @@ public class QueryDebug {
 			if (cs.getHorizontal_head().equals(o) || cs.getVertical_head().equals(o)) {
 				prefix = "HEAD";
 			}
-			String nodeName = prefix + "(" + o.getReferenceCoord() + ")" + 
+			String nodeName = prefix + "L(" + rndbl(o.getReferenceCoord(), 3) + ")" + 
 					o.eClass().getName().substring(5, 9);
 			printer.println(o.hashCode() + " " + nodeName);
 		}
@@ -57,7 +62,7 @@ public class QueryDebug {
 			if (o.getPrevLane() != null){
 				int curName = o.hashCode();
 				int curPrev = o.getPrevLane().hashCode();
-				double edgeLabel = o.getPrevLane().getNumWidth();
+				double edgeLabel = rndbl(o.getPrevLane().getNumWidth(), 1);
 				printer.println(curName + " " + curPrev + " " + edgeLabel);
 			}
 		}
@@ -82,14 +87,14 @@ public class QueryDebug {
 		
 //		ViatraQueryEngine engine = ViatraQueryEngine.on(new EMFScope(rs));		
 //		// Access pattern matcher
-//		CrossingScenarioQueries.instance().prepare(engine);
+//		Queries.instance().prepare(engine);
 //		
-//		Define_referenceCoord_laneWithPrevHasCorrectRefCoord.Matcher matcher = Define_referenceCoord_laneWithPrevHasCorrectRefCoord.Matcher.on(engine);
+//		X.Matcher matcher = X.Matcher.on(engine);
 //		// Get and iterate over all matches
 //		System.out.println("MATCHES:");
-//		for (Define_referenceCoord_laneWithPrevHasCorrectRefCoord.Match match : matcher.getAllMatches()) {
+//		for (X.Match match : matcher.getAllMatches()) {
 //			// Print all the matches to the standard output
-//			System.out.println(match.getL());
+//			System.out.println(match.getP());
 //		}
 	}
 	
-- 
cgit v1.2.3-54-g00ecf