aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorLibravatar Aren Babikian <aren.babikian@mail.mcgill.ca>2021-02-16 09:01:25 +0100
committerLibravatar Aren Babikian <aren.babikian@mail.mcgill.ca>2021-02-16 09:01:25 +0100
commitbc403272d867f82edd623179d82c080e57154c1a (patch)
tree3551ba142ed725595ee684981fc8973cade2ebf4
parentadd dreal-timeout flag (diff)
downloadVIATRA-Generator-bc403272d867f82edd623179d82c080e57154c1a.tar.gz
VIATRA-Generator-bc403272d867f82edd623179d82c080e57154c1a.tar.zst
VIATRA-Generator-bc403272d867f82edd623179d82c080e57154c1a.zip
CrossingScenario case study is ready for serverdreal-integration
Diffstat
-rw-r--r--Domains/crossingScenario/src/crossingScenario/run/DrawScenario.java10
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend2
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java3
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java4
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend6
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java15
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java1
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend10
-rw-r--r--Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/objectives/impl/ModelQueriesGlobalConstraint.java2
-rw-r--r--Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/solutionstore/SolutionStore.java3
-rw-r--r--Tests/MODELS2020-CaseStudies/case.study.pledge.run/RunGeneratorConfig.jarbin78139397 -> 78169348 bytes
-rw-r--r--Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericCrossScenario.vsconfig51
-rw-r--r--Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyNo.vsconfig64
-rw-r--r--Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyNoWithHints.vsconfig64
-rw-r--r--Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyYes.vsconfig65
-rw-r--r--Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/crossScen4Strat.xmi38
-rw-r--r--Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/crossScen5.xmi31
-rw-r--r--Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesScale.vql220
-rw-r--r--Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategy.vql646
-rw-r--r--Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategyHints.vql646
-rwxr-xr-xTests/MODELS2020-CaseStudies/case.study.pledge.run/runCrossScenario.sh21
-rwxr-xr-xTests/MODELS2020-CaseStudies/case.study.pledge.run/runCrossScenarioStrategy.sh15
-rwxr-xr-xTests/MODELS2020-CaseStudies/case.study.pledge.run/runTestCrossScenario.sh11
-rw-r--r--Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend18
24 files changed, 1925 insertions, 21 deletions
diff --git a/Domains/crossingScenario/src/crossingScenario/run/DrawScenario.java b/Domains/crossingScenario/src/crossingScenario/run/DrawScenario.java
index cce2b3f2..61fa51a2 100644
--- a/Domains/crossingScenario/src/crossingScenario/run/DrawScenario.java
+++ b/Domains/crossingScenario/src/crossingScenario/run/DrawScenario.java
@@ -32,10 +32,12 @@ public class DrawScenario {
32 public static final int SIZE = 1000; 32 public static final int SIZE = 1000;
33 33
34 public static void main(String[] args) throws IOException { 34 public static void main(String[] args) throws IOException {
35 for (int i = 1; i <= 10; i++) { 35 drawScenario("/home/models/VIATRA-Generator/Tests/MODELS2020-CaseStudies/case.study.pledge.run/measurements/models/StrategyNo/size01to-1r1n1rt300nsdreal-localdrto10000_16-0823/1.xmi"
36 drawScenario("outputs/models/"+i+".xmi", "outputs/drawnModel"+i+".png"); 36 , "outputs/drawnModelMisc.png");
37 System.out.println("DONE " + i); 37// for (int i = 1; i <= 10; i++) {
38 } 38// drawScenario("outputs/models/"+i+".xmi", "outputs/drawnModel"+i+".png");
39// System.out.println("DONE " + i);
40// }
39 } 41 }
40 42
41 public static File drawScenario(String pathToXmi, String saveToPath) throws IOException { 43 public static File drawScenario(String pathToXmi, String saveToPath) throws IOException {
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend
index ae94c327..f8d3e3bd 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend
@@ -21,7 +21,7 @@ class ExpressionEvaluation2Logic {
21 def getNumericSolver() { 21 def getNumericSolver() {
22 if(_numericSolver === null) { 22 if(_numericSolver === null) {
23 // it seems like this getter has no use 23 // it seems like this getter has no use
24 _numericSolver = (new NumericTranslator(null)).selectProblemSolver("z3") 24 _numericSolver = (new NumericTranslator(null, 0)).selectProblemSolver("z3")
25 } 25 }
26 return _numericSolver 26 return _numericSolver
27 } 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 eb63d96a..cecd3623 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
@@ -44,7 +44,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
44 44
45 private final int TIMEOUT_DOCKER = 5000; 45 private final int TIMEOUT_DOCKER = 5000;
46 private int TIMEOUT_LOCAL = -1; 46 private int TIMEOUT_LOCAL = -1;
47 private final int DEBUG_PRINT = 2; 47 private final int DEBUG_PRINT = 0;
48 48
49 public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath, int drealTimeout) throws IOException, InterruptedException { 49 public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath, int drealTimeout) throws IOException, InterruptedException {
50 this.useDocker = useDocker; 50 this.useDocker = useDocker;
@@ -72,6 +72,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
72 private Process runProcess(List<String> cmd, int timeout) throws IOException, InterruptedException { 72 private Process runProcess(List<String> cmd, int timeout) throws IOException, InterruptedException {
73// String s = String.join(" ", cmd); 73// String s = String.join(" ", cmd);
74// Process p = Runtime.getRuntime().exec(s); 74// Process p = Runtime.getRuntime().exec(s);
75 Runtime.getRuntime().exec("killall -9 dreal").waitFor();
75 Process p = (new ProcessBuilder(cmd)).start(); 76 Process p = (new ProcessBuilder(cmd)).start();
76// p.waitFor(); 77// p.waitFor();
77 //TODO timeout if needed 78 //TODO timeout if needed
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java
index 1e5c1f29..e8c20138 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java
@@ -13,16 +13,18 @@ public class NumericDynamicProblemSolver extends NumericProblemSolver{
13 13
14// private NumericZ3ProblemSolver z3Solver; 14// private NumericZ3ProblemSolver z3Solver;
15 private NumericDrealProblemSolver drealSolver; 15 private NumericDrealProblemSolver drealSolver;
16 private int timeout;
16 17
17 public NumericDynamicProblemSolver(String drealLocalPath, int drealTimeout) throws IOException, InterruptedException { 18 public NumericDynamicProblemSolver(String drealLocalPath, int drealTimeout) throws IOException, InterruptedException {
18// this.z3Solver = new NumericZ3ProblemSolver(); 19// this.z3Solver = new NumericZ3ProblemSolver();
19 this.drealSolver = new NumericDrealProblemSolver(false, drealLocalPath, drealTimeout); 20 this.drealSolver = new NumericDrealProblemSolver(false, drealLocalPath, drealTimeout);
21 this.timeout = drealTimeout;
20 } 22 }
21 23
22 public NumericProblemSolver selectSolver(String selection) { 24 public NumericProblemSolver selectSolver(String selection) {
23 switch (selection) { 25 switch (selection) {
24 case "z3": 26 case "z3":
25 return new NumericZ3ProblemSolver(); 27 return new NumericZ3ProblemSolver(timeout);
26 case "dreal": 28 case "dreal":
27 return this.drealSolver; 29 return this.drealSolver;
28 default: 30 default:
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend
index 791dd644..a11ae8a8 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend
@@ -17,6 +17,7 @@ class NumericTranslator {
17 17
18 private XExpressionExtractor extractor = new XExpressionExtractor(); 18 private XExpressionExtractor extractor = new XExpressionExtractor();
19 private NumericProblemSolver numericSolver; 19 private NumericProblemSolver numericSolver;
20 private int timeout;
20 21
21 long formingProblemTime=0; 22 long formingProblemTime=0;
22 long solvingProblemTime=0; 23 long solvingProblemTime=0;
@@ -29,8 +30,9 @@ class NumericTranslator {
29 } 30 }
30 } 31 }
31 32
32 new(NumericProblemSolver numericProblemSolver){ 33 new(NumericProblemSolver numericProblemSolver, int timeout){
33 this.numericSolver = numericProblemSolver 34 this.numericSolver = numericProblemSolver
35 this.timeout = timeout;
34 } 36 }
35 37
36 def Map<JvmIdentifiableElement, PrimitiveElement> arrayToMap(Object[] tuple, ArrayList<JvmIdentifiableElement> variablesInOrder) { 38 def Map<JvmIdentifiableElement, PrimitiveElement> arrayToMap(Object[] tuple, ArrayList<JvmIdentifiableElement> variablesInOrder) {
@@ -63,7 +65,7 @@ class NumericTranslator {
63 val NumericDynamicProblemSolver dynamicSolver = numericSolver as NumericDynamicProblemSolver 65 val NumericDynamicProblemSolver dynamicSolver = numericSolver as NumericDynamicProblemSolver
64 return dynamicSolver.selectSolver(selection); 66 return dynamicSolver.selectSolver(selection);
65 } else{ 67 } else{
66 if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver 68 if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver(this.timeout)
67 return numericSolver; 69 return numericSolver;
68 } 70 }
69 } 71 }
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java
index 612e93a6..0799953f 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java
@@ -1,6 +1,5 @@
1package hu.bme.mit.inf.dslreasoner.viatra2logic; 1package hu.bme.mit.inf.dslreasoner.viatra2logic;
2 2
3import java.io.File;
4import java.util.ArrayList; 3import java.util.ArrayList;
5import java.util.HashMap; 4import java.util.HashMap;
6import java.util.List; 5import java.util.List;
@@ -20,6 +19,7 @@ import com.microsoft.z3.Context;
20import com.microsoft.z3.Expr; 19import com.microsoft.z3.Expr;
21import com.microsoft.z3.IntExpr; 20import com.microsoft.z3.IntExpr;
22import com.microsoft.z3.Model; 21import com.microsoft.z3.Model;
22import com.microsoft.z3.Params;
23import com.microsoft.z3.RealExpr; 23import com.microsoft.z3.RealExpr;
24import com.microsoft.z3.Solver; 24import com.microsoft.z3.Solver;
25import com.microsoft.z3.Status; 25import com.microsoft.z3.Status;
@@ -36,7 +36,7 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{
36 private Solver s; 36 private Solver s;
37 private Map<Object, Expr> varMap; 37 private Map<Object, Expr> varMap;
38 38
39 public NumericZ3ProblemSolver() { 39 public NumericZ3ProblemSolver(int timeout) {
40 //FOR LINUX VM 40 //FOR LINUX VM
41 //Not Elegant, but this is working for now 41 //Not Elegant, but this is working for now
42// String root = "/home/models/VIATRA-Generator"; 42// String root = "/home/models/VIATRA-Generator";
@@ -50,6 +50,11 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{
50 ctx = new Context(cfg); 50 ctx = new Context(cfg);
51 ctx.setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB_FULL); 51 ctx.setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB_FULL);
52 s = ctx.mkSolver(); 52 s = ctx.mkSolver();
53 if (timeout != -1) {
54 Params p = ctx.mkParams();
55 p.add("timeout", timeout);
56 s.setParameters(p);
57 }
53 varMap = new HashMap<Object, Expr>(); 58 varMap = new HashMap<Object, Expr>();
54 } 59 }
55 60
@@ -82,7 +87,11 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{
82 s.add(problemInstance); 87 s.add(problemInstance);
83 endformingProblem = System.nanoTime()-startformingProblem; 88 endformingProblem = System.nanoTime()-startformingProblem;
84 long startSolvingProblem = System.nanoTime(); 89 long startSolvingProblem = System.nanoTime();
85 boolean result = (s.check() == Status.SATISFIABLE); 90// System.out.print("start - ");
91 Status soln = s.check();
92 boolean result = (soln == Status.SATISFIABLE);
93 if (soln == Status.UNKNOWN) System.err.println("TIMEOUT");
94// System.out.println("end");
86 endSolvingProblem = System.nanoTime()-startSolvingProblem; 95 endSolvingProblem = System.nanoTime()-startSolvingProblem;
87 this.ctx.close(); 96 this.ctx.close();
88 return result; 97 return result;
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
index a8d2381c..c62d124a 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
@@ -222,6 +222,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
222// } 222// }
223// } 223// }
224 224
225// System.out.println("--------NEXT");
225 boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFitness); 226 boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFitness);
226 if(consistencyCheckResult == true) { continue mainLoop; } 227 if(consistencyCheckResult == true) { continue mainLoop; }
227 228
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 8281c3c3..a228afc6 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
@@ -55,7 +55,7 @@ class NumericSolver {
55 this.caching = caching 55 this.caching = caching
56 this.drealLocalPath = config.drealLocalPath 56 this.drealLocalPath = config.drealLocalPath
57 this.strategy = config.strategy 57 this.strategy = config.strategy
58 this.t = new NumericTranslator(createNumericTranslator(config)) 58 this.t = new NumericTranslator(createNumericTranslator(config), config.drealTimeout)
59 } 59 }
60 60
61 def createNumericTranslator(ViatraReasonerConfiguration config) { 61 def createNumericTranslator(ViatraReasonerConfiguration config) {
@@ -77,7 +77,7 @@ class NumericSolver {
77 System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); 77 System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so");
78 // System.load("libz3.so"); 78 // System.load("libz3.so");
79 // System.load("libz3java.so"); 79 // System.load("libz3java.so");
80 return new NumericZ3ProblemSolver 80 return new NumericZ3ProblemSolver(config.drealTimeout)
81 } 81 }
82 } 82 }
83 else { 83 else {
@@ -150,9 +150,9 @@ class NumericSolver {
150 //Filter constraints if there are phase-related restricutions 150 //Filter constraints if there are phase-related restricutions
151 //null whitelist means accept everything 151 //null whitelist means accept everything
152 152
153 println("<<<<START-STEP>>>> (" + phase + ")") 153// println("<<<<START-STEP>>>> (" + phase + ")")
154 if (phase == -2) { 154 if (phase == -2) {
155 println("Skipping numeric check") 155// println("Skipping numeric check")
156 //TODO Big assumption 156 //TODO Big assumption
157 return true 157 return true
158 } 158 }
@@ -235,7 +235,7 @@ class NumericSolver {
235 235
236 def selectSolver(int phase) { 236 def selectSolver(int phase) {
237 if (strategy === ExplorationStrategy.CrossingScenario){ 237 if (strategy === ExplorationStrategy.CrossingScenario){
238 if (phase == 1) return "dreal" 238 if (phase == 1) return "z3"
239 else return "dreal" 239 else return "dreal"
240 } 240 }
241 return "irrelevant" 241 return "irrelevant"
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/objectives/impl/ModelQueriesGlobalConstraint.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/objectives/impl/ModelQueriesGlobalConstraint.java
index 7616b4a2..3a990a1e 100644
--- a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/objectives/impl/ModelQueriesGlobalConstraint.java
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/objectives/impl/ModelQueriesGlobalConstraint.java
@@ -87,6 +87,8 @@ public class ModelQueriesGlobalConstraint implements IGlobalConstraint {
87 for (ViatraQueryMatcher<? extends IPatternMatch> matcher : matchers) { 87 for (ViatraQueryMatcher<? extends IPatternMatch> matcher : matchers) {
88 if ((type.equals(ModelQueryType.NO_MATCH) && matcher.countMatches() > 0) 88 if ((type.equals(ModelQueryType.NO_MATCH) && matcher.countMatches() > 0)
89 || (type.equals(ModelQueryType.MUST_HAVE_MATCH) && matcher.countMatches() == 0)) { 89 || (type.equals(ModelQueryType.MUST_HAVE_MATCH) && matcher.countMatches() == 0)) {
90// System.out.println(type + " " + matcher.countMatches());
91// System.out.println(matcher.getSpecification().getSimpleName());
90 return false; 92 return false;
91 } 93 }
92 } 94 }
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/solutionstore/SolutionStore.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/solutionstore/SolutionStore.java
index 578ae277..6e0abd0b 100644
--- a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/solutionstore/SolutionStore.java
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/solutionstore/SolutionStore.java
@@ -208,10 +208,11 @@ public class SolutionStore {
208 solutionTrajectory.setFitness(fitness); 208 solutionTrajectory.setFitness(fitness);
209 209
210 if (acceptOnlyGoalSolutions && !fitness.isSatisifiesHardObjectives()) { 210 if (acceptOnlyGoalSolutions && !fitness.isSatisifiesHardObjectives()) {
211// System.out.println("NOT SAVING");
211 unsavedSolutionCallbacks(context, solutionTrajectory); 212 unsavedSolutionCallbacks(context, solutionTrajectory);
212 return; 213 return;
213 } 214 }
214 215 System.out.println("SAVING SOLUTION");
215 boolean solutionSaved = solutionSaver.saveSolution(context, id, solutionTrajectory); 216 boolean solutionSaved = solutionSaver.saveSolution(context, id, solutionTrajectory);
216 217
217 if (solutionSaved) { 218 if (solutionSaved) {
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/RunGeneratorConfig.jar b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/RunGeneratorConfig.jar
index 8d981fde..b97ebf5c 100644
--- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/RunGeneratorConfig.jar
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/RunGeneratorConfig.jar
Binary files differ
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericCrossScenario.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericCrossScenario.vsconfig
new file mode 100644
index 00000000..290b8835
--- /dev/null
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericCrossScenario.vsconfig
@@ -0,0 +1,51 @@
1import epackage "../../../Domains/crossingScenario/model/crossingScenario.ecore"
2import viatra "queries/csQueriesScale.vql"
3import epackage "../../../Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/model/satellite.ecore"
4import viatra "queries/SatelliteQueries.vql"
5
6generate {
7 metamodel = { package satellite }
8 constraints = { package hu.bme.mit.inf.dslreasoner.domains.satellite.queries }
9 partial-model = { "inputs/SatelliteInstance.xmi"}
10 solver = ViatraSolver
11 scope = {
12 #node += 10..*
13 }
14
15 config = {
16 runtime = 10000,
17 "numeric-solver" = "z3",
18 log-level = none
19 }
20
21 runs = 1
22
23 output = "measurements/debug/warmup"
24}
25
26generate {
27 metamodel = { package crossingScenario }
28 constraints = { package queries}
29 partial-model = { "inputs/crossScen5.xmi"}
30 solver = ViatraSolver
31 scope = {
32 #node += 3..*
33 ,#<Lane> += 0
34 ,#<Relation> += 0
35 }
36
37 config = {
38 runtime = 10000,
39 "numeric-solver" = "z3",
40 "dreal-local-path" = "enterPathHere",
41 "dreal-timeout" = "10000",
42 log-level = none,
43 "scopePropagator" = "polyhedral"}
44
45 runs = 1
46 number = 10
47 debug = "outputs/debug"
48 log = "outputs/debug/log.txt"
49 output = "outputs/models"
50 statistics = "outputs/debug/statistics.csv"
51}
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyNo.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyNo.vsconfig
new file mode 100644
index 00000000..836b6b76
--- /dev/null
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyNo.vsconfig
@@ -0,0 +1,64 @@
1import epackage "../../../Domains/crossingScenario/model/crossingScenario.ecore"
2import viatra "queries/csQueriesStrategy.vql"
3import epackage "../../../Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/model/satellite.ecore"
4import viatra "queries/SatelliteQueries.vql"
5
6generate {
7 metamodel = { package satellite }
8 constraints = { package hu.bme.mit.inf.dslreasoner.domains.satellite.queries }
9 partial-model = { "inputs/SatelliteInstance.xmi"}
10 solver = ViatraSolver
11 scope = {
12 #node += 10..*
13 }
14
15 config = {
16 runtime = 10000,
17 "numeric-solver" = "z3",
18 log-level = none
19 }
20
21 runs = 1
22
23 output = "measurements/debug/warmup"
24}
25
26generate {
27 metamodel = { package crossingScenario }
28 constraints = { package queries}
29 partial-model = { "inputs/crossScen4Strat.xmi"}
30 solver = ViatraSolver
31 scope = {
32 #node += 0..*
33 ,#<Lane> += 0
34 ,#<Relation> += 0
35 }
36
37 config = {
38 runtime = 10000,
39 "numeric-solver" = "z3",
40 "dreal-local-path" = "enterPathHere",
41 "dreal-timeout" = "10000",
42 log-level = none,
43 "ignored-attributes" = "
44 Pedestrian.xPos=*,
45 Pedestrian.yPos=*,
46 Pedestrian.length=*,
47 Pedestrian.width=*,
48 Pedestrian.xSpeed=*,
49 Pedestrian.ySpeed=*,
50 Vehicle.xPos=*,
51 Vehicle.yPos=*,
52 Vehicle.length=*,
53 Vehicle.width=*,
54 Vehicle.xSpeed=*,
55 Vehicle.ySpeed=*,
56 CollisionExists.collisionTime=*"}
57
58 runs = 1
59 number = 10
60 debug = "outputs/debug"
61 log = "outputs/debug/log.txt"
62 output = "outputs/models"
63 statistics = "outputs/debug/statistics.csv"
64}
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyNoWithHints.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyNoWithHints.vsconfig
new file mode 100644
index 00000000..ebb2c4ca
--- /dev/null
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyNoWithHints.vsconfig
@@ -0,0 +1,64 @@
1import epackage "../../../Domains/crossingScenario/model/crossingScenario.ecore"
2import viatra "queries/csQueriesStrategyHints.vql"
3import epackage "../../../Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/model/satellite.ecore"
4import viatra "queries/SatelliteQueries.vql"
5
6generate {
7 metamodel = { package satellite }
8 constraints = { package hu.bme.mit.inf.dslreasoner.domains.satellite.queries }
9 partial-model = { "inputs/SatelliteInstance.xmi"}
10 solver = ViatraSolver
11 scope = {
12 #node += 10..*
13 }
14
15 config = {
16 runtime = 10000,
17 "numeric-solver" = "z3",
18 log-level = none
19 }
20
21 runs = 1
22
23 output = "measurements/debug/warmup"
24}
25
26generate {
27 metamodel = { package crossingScenario }
28 constraints = { package queries}
29 partial-model = { "inputs/crossScen4Strat.xmi"}
30 solver = ViatraSolver
31 scope = {
32 #node += 0..*
33 ,#<Lane> += 0
34 ,#<Relation> += 0
35 }
36
37 config = {
38 runtime = 10000,
39 "numeric-solver" = "z3",
40 "dreal-local-path" = "enterPathHere",
41 "dreal-timeout" = "10000",
42 log-level = none,
43 "ignored-attributes" = "
44 Pedestrian.xPos=*,
45 Pedestrian.yPos=*,
46 Pedestrian.length=*,
47 Pedestrian.width=*,
48 Pedestrian.xSpeed=*,
49 Pedestrian.ySpeed=*,
50 Vehicle.xPos=*,
51 Vehicle.yPos=*,
52 Vehicle.length=*,
53 Vehicle.width=*,
54 Vehicle.xSpeed=*,
55 Vehicle.ySpeed=*,
56 CollisionExists.collisionTime=*"}
57
58 runs = 1
59 number = 10
60 debug = "outputs/debug"
61 log = "outputs/debug/log.txt"
62 output = "outputs/models"
63 statistics = "outputs/debug/statistics.csv"
64}
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyYes.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyYes.vsconfig
new file mode 100644
index 00000000..5c2077c2
--- /dev/null
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyYes.vsconfig
@@ -0,0 +1,65 @@
1import epackage "../../../Domains/crossingScenario/model/crossingScenario.ecore"
2import viatra "queries/csQueriesStrategy.vql"
3import epackage "../../../Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/model/satellite.ecore"
4import viatra "queries/SatelliteQueries.vql"
5
6generate {
7 metamodel = { package satellite }
8 constraints = { package hu.bme.mit.inf.dslreasoner.domains.satellite.queries }
9 partial-model = { "inputs/SatelliteInstance.xmi"}
10 solver = ViatraSolver
11 scope = {
12 #node += 10..*
13 }
14
15 config = {
16 runtime = 10000,
17 "numeric-solver" = "z3",
18 log-level = none
19 }
20
21 runs = 1
22
23 output = "measurements/debug/warmup"
24}
25
26generate {
27 metamodel = { package crossingScenario }
28 constraints = { package queries}
29 partial-model = { "inputs/crossScen4Strat.xmi"}
30 solver = ViatraSolver
31 scope = {
32 #node += 0..*
33 ,#<Lane> += 0
34 ,#<Relation> += 0
35 }
36
37 config = {
38 runtime = 10000,
39 "numeric-solver" = "z3",
40 "dreal-local-path" = "enterPathHere",
41 "dreal-timeout" = "10000",
42 log-level = none,
43 "strategy" = "crossingScenario",
44 "ignored-attributes" = "
45 Pedestrian.xPos=*,
46 Pedestrian.yPos=*,
47 Pedestrian.length=*,
48 Pedestrian.width=*,
49 Pedestrian.xSpeed=*,
50 Pedestrian.ySpeed=*,
51 Vehicle.xPos=*,
52 Vehicle.yPos=*,
53 Vehicle.length=*,
54 Vehicle.width=*,
55 Vehicle.xSpeed=*,
56 Vehicle.ySpeed=*,
57 CollisionExists.collisionTime=*"}
58
59 runs = 1
60 number = 10
61 debug = "outputs/debug"
62 log = "outputs/debug/log.txt"
63 output = "outputs/models"
64 statistics = "outputs/debug/statistics.csv"
65}
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/crossScen4Strat.xmi b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/crossScen4Strat.xmi
new file mode 100644
index 00000000..08cde1e8
--- /dev/null
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/crossScen4Strat.xmi
@@ -0,0 +1,38 @@
1<?xml version="1.0" encoding="UTF-8"?>
2<crossingScenario:CrossingScenario
3 xmi:version="2.0"
4 xmlns:xmi="http://www.omg.org/XMI"
5 xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
6 xmlns:crossingScenario="http://www.example.com/crossingScenario"
7 xsi:schemaLocation="http://www.example.com/crossingScenario ../model/crossingScenario.ecore"
8 xSize="30.0"
9 ySize="30.0"
10 maxTime="60.0"
11 maxXSpeed="100.0"
12 maxYSpeed="100.0">
13 <actors xsi:type="crossingScenario:Pedestrian"/>
14 <actors xsi:type="crossingScenario:Vehicle"/>
15 <lanes xsi:type="crossingScenario:Lane_Horizontal"/>
16 <lanes xsi:type="crossingScenario:Lane_Horizontal"
17 referenceCoord="3.0"/>
18 <lanes xsi:type="crossingScenario:Lane_Horizontal"
19 referenceCoord="6.0"/>
20 <lanes xsi:type="crossingScenario:Lane_Horizontal"
21 referenceCoord="9.0"/>
22 <lanes xsi:type="crossingScenario:Lane_Vertical"/>
23 <lanes xsi:type="crossingScenario:Lane_Vertical"
24 referenceCoord="3.0"/>
25 <lanes xsi:type="crossingScenario:Lane_Vertical"
26 referenceCoord="6.0"/>
27 <lanes xsi:type="crossingScenario:Lane_Vertical"
28 referenceCoord="9.0"/>
29 <relations
30 xsi:type="crossingScenario:CollisionExists"
31 target="//@actors.0"
32 source="//@actors.1"
33 collisionTime="-1.0"/>
34 <relations
35 xsi:type="crossingScenario:VisionBlocked"
36 target="//@actors.0"
37 source="//@actors.1"/>
38</crossingScenario:CrossingScenario>
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/crossScen5.xmi b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/crossScen5.xmi
new file mode 100644
index 00000000..5eee1734
--- /dev/null
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/crossScen5.xmi
@@ -0,0 +1,31 @@
1<?xml version="1.0" encoding="UTF-8"?>
2<crossingScenario:CrossingScenario
3 xmi:version="2.0"
4 xmlns:xmi="http://www.omg.org/XMI"
5 xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
6 xmlns:crossingScenario="http://www.example.com/crossingScenario"
7 xsi:schemaLocation="http://www.example.com/crossingScenario ../model/crossingScenario.ecore"
8 xSize="30.0"
9 ySize="30.0"
10 maxTime="60.0"
11 maxXSpeed="10.0"
12 maxYSpeed="10.0">
13 <lanes xsi:type="crossingScenario:Lane_Horizontal"/>
14 <lanes xsi:type="crossingScenario:Lane_Horizontal"
15 referenceCoord="3.0"/>
16 <lanes xsi:type="crossingScenario:Lane_Horizontal"
17 referenceCoord="6.0"/>
18 <lanes xsi:type="crossingScenario:Lane_Horizontal"
19 referenceCoord="9.0"/>
20 <lanes xsi:type="crossingScenario:Lane_Horizontal"
21 referenceCoord="12.0"/>
22 <lanes xsi:type="crossingScenario:Lane_Vertical"/>
23 <lanes xsi:type="crossingScenario:Lane_Vertical"
24 referenceCoord="3.0"/>
25 <lanes xsi:type="crossingScenario:Lane_Vertical"
26 referenceCoord="6.0"/>
27 <lanes xsi:type="crossingScenario:Lane_Vertical"
28 referenceCoord="9.0"/>
29 <lanes xsi:type="crossingScenario:Lane_Vertical"
30 referenceCoord="12.0"/>
31</crossingScenario:CrossingScenario>
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesScale.vql b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesScale.vql
new file mode 100644
index 00000000..d3afa775
--- /dev/null
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesScale.vql
@@ -0,0 +1,220 @@
1package queries
2
3import "http://www.example.com/crossingScenario"
4import "http://www.eclipse.org/emf/2002/Ecore"
5
6///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
7//Lane+Actor
8///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
9
10/////////Actor (a) on vertical lane (l) must have a.xPos=[l.rc, l.rc + l.nw]
11@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes")
12pattern define_placedOn_actorOnVerticalLane(a : Actor, vl:Lane_Vertical) {
13 Actor.placedOn(a, vl);
14 Actor.xPos(a, x);
15 Lane.referenceCoord(vl, r);
16 check(x <= r);
17} or {
18 Actor.placedOn(a, vl);
19 Actor.xPos(a, x);
20 Lane.referenceCoord(vl, r);
21// //<<<<OLD>>>>
22// Lane.numWidth(vl, w);
23// check(x >= (r + w));
24
25 //<<<<NEW>>>>: lanes all have width=3
26 check(x >= (r + 3.0));
27}
28
29@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes")
30pattern define_placedOn_actorOnHorizLane(a : Actor, hl:Lane_Horizontal) {
31 Actor.placedOn(a, hl);
32 Actor.yPos(a, y);
33 Lane.referenceCoord(hl, r);
34 check(y <= r);
35} or {
36 Actor.placedOn(a, hl);
37 Actor.yPos(a, y);
38 Lane.referenceCoord(hl, r);
39// //<<OLD>>
40// Lane.numWidth(hl, w);
41// check(y >= (r + w));
42
43 //<<NEW>>: lanes all have width=3
44 check(y >= (r + 3.0));
45
46}
47
48///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
49//Actor
50///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
51
52/////----------------
53//Xpos and Ypos Bounds
54/////----------------
55
56private pattern helper_horiz_getXAndBounds(cs:CrossingScenario, a:Actor,
57 xMax:java Double, xP:java Double) {
58 Actor.placedOn(a, hl);
59 Lane_Horizontal(hl);
60 CrossingScenario.actors(cs, a);
61 CrossingScenario.xSize(cs, xMax);
62 Actor.xPos(a, xP);
63}
64
65private pattern helper_vert_getYAndBounds(cs:CrossingScenario, a:Actor,
66 yMax:java Double, yP:java Double) {
67 Actor.placedOn(a, vl);
68 Lane_Vertical(vl);
69 CrossingScenario.actors(cs, a);
70 CrossingScenario.ySize(cs, yMax);
71 Actor.yPos(a, yP);
72}
73
74@Constraint(severity="error", key={cs}, message="x")
75pattern define_actor_maxXp(cs:CrossingScenario, a:Actor) {
76 find helper_horiz_getXAndBounds(cs, a, xMax, xP);
77 check(xP >= xMax);}
78
79@Constraint(severity="error", key={cs}, message="x")
80pattern define_actor_minXp(cs:CrossingScenario, a:Actor) {
81 find helper_horiz_getXAndBounds(cs, a, xMax, xP);
82 check(xP <= 0-xMax);}
83
84@Constraint(severity="error", key={cs}, message="x")
85pattern define_actor_maxYp(cs:CrossingScenario, a:Actor) {
86 find helper_vert_getYAndBounds(cs, a, yMax, yP);
87 check(yP >= yMax);}
88
89@Constraint(severity="error", key={cs}, message="x")
90pattern define_actor_minYp(cs:CrossingScenario, a:Actor) {
91 find helper_vert_getYAndBounds(cs, a, yMax, yP);
92 check(yP <= 0-yMax);}
93
94//Minimum Distances
95private pattern helper_getCoords(a1:Actor,
96 a2: Actor, x1:java Double, x2:java Double, y1:java Double, y2:java Double) {
97 Actor.xPos(a1, x1);
98 Actor.yPos(a1, y1);
99 Actor.xPos(a2, x2);
100 Actor.yPos(a2, y2);
101}
102
103//INFO may remove?
104@Constraint(severity="error", key={a1, a2}, message="x")
105pattern define_actor_minimumDistance(a1: Actor, a2: Actor) {
106 find helper_getCoords(a1, a2, x1, x2, y1, y2);
107 a1 != a2;
108 //check(dx^2 + dy^2 < 4^2)
109 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 4*4);
110}
111
112/////----------------
113//Xspeed and Yspeed bounds
114/////----------------
115/*
116/////////VERTICAL LANE
117@Constraint(severity="error", key={a}, message="7 Actor")
118pattern define_actor_actorOnVertLaneHasxSpeed0(a:Actor) {
119 Actor.placedOn(a, vl);
120 Lane_Vertical(vl);
121 Actor.xSpeed(a, xSpeed);
122 check(xSpeed != 0.0);
123}
124
125private pattern helper_vert_getYSpeedAndBounds(cs:CrossingScenario, a:Actor,
126 ySpeedMax:java Double, ySpeed:java Double) {
127 Actor.placedOn(a, vl);
128 Lane_Vertical(vl);
129 CrossingScenario.actors(cs, a);
130 CrossingScenario.maxYSpeed(cs, ySpeedMax);
131 Actor.ySpeed(a, ySpeed);
132}
133
134@Constraint(severity="error", key={cs}, message="x")
135pattern define_actor_actorOnVertLaneMinYs(cs:CrossingScenario, a:Actor) {
136 find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS);
137 check(yS <= 0.0-ySMax);
138}
139
140@Constraint(severity="error", key={cs}, message="x")
141pattern define_actor_actorOnVertLaneMaxYs(cs:CrossingScenario, a:Actor) {
142 find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS);
143 check(yS >= ySMax);
144}
145
146/////////HORIZONTAL LANE
147@Constraint(severity="error", key={a}, message="7 Actor")
148pattern define_actor_actorOnHorizLaneHasySpeed0(a:Actor) {
149 Actor.placedOn(a, hl);
150 Lane_Horizontal(hl);
151 Actor.ySpeed(a, ySpeed);
152 check(ySpeed != 0.0);
153}
154
155private pattern helper_horiz_getXSpeedAndBounds(cs:CrossingScenario, a:Actor,
156 xSpeedMax:java Double, xSpeed:java Double) {
157 Actor.placedOn(a, hl);
158 Lane_Horizontal(hl);
159 CrossingScenario.actors(cs, a);
160 CrossingScenario.maxXSpeed(cs, xSpeedMax);
161 Actor.xSpeed(a, xSpeed);
162}
163
164@Constraint(severity="error", key={cs}, message="x")
165pattern define_actor_actorOnHorizLaneMinXs(cs:CrossingScenario, a:Actor) {
166 find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS);
167 check(xS <= 0.0-xSMax);
168}
169
170@Constraint(severity="error", key={cs}, message="x")
171pattern define_actor_actorOnHorizLaneMaxXs(cs:CrossingScenario, a:Actor) {
172 find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS);
173 check(xS >= xSMax);
174}
175*/
176/////----------------
177/////WIDTH and LENGTH
178/////----------------
179
180///////pedestrian-width (3)
181@Constraint(severity="error", key={p}, message="3 Actor")
182pattern define_actor_pedestrianWidth(p:Pedestrian) {
183 Pedestrian.width(p, w);
184 check(w != 1.0);
185}
186
187/////////pedestrian-width (4)
188@Constraint(severity="error", key={p}, message="4 Actor")
189pattern define_actor_pedestrianLength(p:Pedestrian) {
190 Pedestrian.length(p, l);
191 check(l != 1.0);
192}
193
194/////////actor-width (5)
195@Constraint(severity="error", key={v}, message="5 Actor")
196pattern define_actor_vehicleWidth(v:Vehicle) {
197 Vehicle.placedOn(v, lane);
198 Lane_Vertical(lane);
199 Vehicle.width(v, w);
200 check(w != 2.0);
201} or {
202 Vehicle.placedOn(v, lane);
203 Lane_Horizontal(lane);
204 Vehicle.width(v, w);
205 check(w != 3.0);
206}
207
208/////////actor-width (6)
209@Constraint(severity="error", key={v}, message="6 Actor")
210pattern define_actor_vehicleLength(v:Vehicle) {
211 Vehicle.placedOn(v, lane);
212 Lane_Vertical(lane);
213 Vehicle.length(v, l);
214 check(l != 3.0);
215} or {
216 Vehicle.placedOn(v, lane);
217 Lane_Horizontal(lane);
218 Vehicle.length(v, l);
219 check(l != 2.0);
220}
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategy.vql b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategy.vql
new file mode 100644
index 00000000..5f35cd2b
--- /dev/null
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategy.vql
@@ -0,0 +1,646 @@
1package queries
2
3import "http://www.example.com/crossingScenario"
4import "http://www.eclipse.org/emf/2002/Ecore"
5
6///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
7//Lane+Actor
8///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
9
10/////////Actor (a) on vertical lane (l) must have a.xPos=[l.rc, l.rc + l.nw]
11@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes")
12pattern define_placedOn_actorOnVerticalLane(a : Actor, vl:Lane_Vertical) {
13 Actor.placedOn(a, vl);
14 Actor.xPos(a, x);
15 Lane.referenceCoord(vl, r);
16 check(x <= r);
17} or {
18 Actor.placedOn(a, vl);
19 Actor.xPos(a, x);
20 Lane.referenceCoord(vl, r);
21// //<<<<OLD>>>>
22// Lane.numWidth(vl, w);
23// check(x >= (r + w));
24
25 //<<<<NEW>>>>: lanes all have width=3
26 check(x >= (r + 3.0));
27}
28
29@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes")
30pattern define_placedOn_actorOnHorizLane(a : Actor, hl:Lane_Horizontal) {
31 Actor.placedOn(a, hl);
32 Actor.yPos(a, y);
33 Lane.referenceCoord(hl, r);
34 check(y <= r);
35} or {
36 Actor.placedOn(a, hl);
37 Actor.yPos(a, y);
38 Lane.referenceCoord(hl, r);
39// //<<OLD>>
40// Lane.numWidth(hl, w);
41// check(y >= (r + w));
42
43 //<<NEW>>: lanes all have width=3
44 check(y >= (r + 3.0));
45
46}
47
48///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
49//Actor
50///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
51
52/////----------------
53//Xpos and Ypos Bounds
54/////----------------
55
56private pattern helper_horiz_getXAndBounds(cs:CrossingScenario, a:Actor,
57 xMax:java Double, xP:java Double) {
58 Actor.placedOn(a, hl);
59 Lane_Horizontal(hl);
60 CrossingScenario.actors(cs, a);
61 CrossingScenario.xSize(cs, xMax);
62 Actor.xPos(a, xP);
63}
64
65private pattern helper_vert_getYAndBounds(cs:CrossingScenario, a:Actor,
66 yMax:java Double, yP:java Double) {
67 Actor.placedOn(a, vl);
68 Lane_Vertical(vl);
69 CrossingScenario.actors(cs, a);
70 CrossingScenario.ySize(cs, yMax);
71 Actor.yPos(a, yP);
72}
73
74@Constraint(severity="error", key={cs}, message="x")
75pattern define_actor_maxXp(cs:CrossingScenario, a:Actor) {
76 find helper_horiz_getXAndBounds(cs, a, xMax, xP);
77 check(xP >= xMax);}
78
79@Constraint(severity="error", key={cs}, message="x")
80pattern define_actor_minXp(cs:CrossingScenario, a:Actor) {
81 find helper_horiz_getXAndBounds(cs, a, xMax, xP);
82 check(xP <= 0-xMax);}
83
84@Constraint(severity="error", key={cs}, message="x")
85pattern define_actor_maxYp(cs:CrossingScenario, a:Actor) {
86 find helper_vert_getYAndBounds(cs, a, yMax, yP);
87 check(yP >= yMax);}
88
89@Constraint(severity="error", key={cs}, message="x")
90pattern define_actor_minYp(cs:CrossingScenario, a:Actor) {
91 find helper_vert_getYAndBounds(cs, a, yMax, yP);
92 check(yP <= 0-yMax);}
93
94////////////ADDED
95//to reduce overlap
96//NEEDED
97/*
98@Constraint(severity="error", key={a}, message="5 Actor")
99pattern define_actor_wrtLane(a:Actor) {
100 Actor.placedOn(a, lane);
101 Lane_Vertical(lane);
102 Actor.yPos(a, yP);
103 check(yP > 0.0-1.0);
104} or {
105 Actor.placedOn(a, lane);
106 Lane_Horizontal(lane);
107 Actor.xPos(a, xP);
108 check(xP > 0.0-1.0);
109}
110*/
111////////////ADDED
112
113//Minimum Distances
114private pattern helper_getCoords(a1:Actor,
115 a2: Actor, x1:java Double, x2:java Double, y1:java Double, y2:java Double) {
116 Actor.xPos(a1, x1);
117 Actor.yPos(a1, y1);
118 Actor.xPos(a2, x2);
119 Actor.yPos(a2, y2);
120}
121
122//INFO may remove?
123@Constraint(severity="error", key={a1, a2}, message="x")
124pattern define_actor_minimumDistance(a1: Actor, a2: Actor) {
125 find helper_getCoords(a1, a2, x1, x2, y1, y2);
126 a1 != a2;
127 //check(dx^2 + dy^2 < 3^2)
128 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 3*3);
129}
130
131/////----------------
132//Xspeed and Yspeed bounds
133/////----------------
134
135/////////VERTICAL LANE
136@Constraint(severity="error", key={a}, message="7 Actor")
137pattern define_actor_actorOnVertLaneHasxSpeed0(a:Actor) {
138 Actor.placedOn(a, vl);
139 Lane_Vertical(vl);
140 Actor.xSpeed(a, xSpeed);
141 check(xSpeed != 0.0);
142}
143
144private pattern helper_vert_getYSpeedAndBounds(cs:CrossingScenario, a:Actor,
145 ySpeedMax:java Double, ySpeed:java Double) {
146 Actor.placedOn(a, vl);
147 Lane_Vertical(vl);
148 CrossingScenario.actors(cs, a);
149 CrossingScenario.maxYSpeed(cs, ySpeedMax);
150 Actor.ySpeed(a, ySpeed);
151}
152
153@Constraint(severity="error", key={cs}, message="x")
154pattern define_actor_actorOnVertLaneMinYs(cs:CrossingScenario, a:Actor) {
155 find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS);
156 check(yS <= 0.0-ySMax);
157}
158
159@Constraint(severity="error", key={cs}, message="x")
160pattern define_actor_actorOnVertLaneMaxYs(cs:CrossingScenario, a:Actor) {
161 find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS);
162 check(yS >= ySMax);
163}
164
165/////////HORIZONTAL LANE
166@Constraint(severity="error", key={a}, message="7 Actor")
167pattern define_actor_actorOnHorizLaneHasySpeed0(a:Actor) {
168 Actor.placedOn(a, hl);
169 Lane_Horizontal(hl);
170 Actor.ySpeed(a, ySpeed);
171 check(ySpeed != 0.0);
172}
173
174private pattern helper_horiz_getXSpeedAndBounds(cs:CrossingScenario, a:Actor,
175 xSpeedMax:java Double, xSpeed:java Double) {
176 Actor.placedOn(a, hl);
177 Lane_Horizontal(hl);
178 CrossingScenario.actors(cs, a);
179 CrossingScenario.maxXSpeed(cs, xSpeedMax);
180 Actor.xSpeed(a, xSpeed);
181}
182
183@Constraint(severity="error", key={cs}, message="x")
184pattern define_actor_actorOnHorizLaneMinXs(cs:CrossingScenario, a:Actor) {
185 find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS);
186 check(xS <= 0.0-xSMax);
187}
188
189@Constraint(severity="error", key={cs}, message="x")
190pattern define_actor_actorOnHorizLaneMaxXs(cs:CrossingScenario, a:Actor) {
191 find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS);
192 check(xS >= xSMax);
193}
194
195/////----------------
196/////WIDTH and LENGTH
197/////----------------
198
199///////pedestrian-width (3)
200@Constraint(severity="error", key={p}, message="3 Actor")
201pattern define_actor_pedestrianWidth(p:Pedestrian) {
202 Pedestrian.width(p, w);
203 check(w != 1.0);
204}
205
206/////////pedestrian-width (4)
207@Constraint(severity="error", key={p}, message="4 Actor")
208pattern define_actor_pedestrianLength(p:Pedestrian) {
209 Pedestrian.length(p, l);
210 check(l != 1.0);
211}
212
213/////////actor-width (5)
214@Constraint(severity="error", key={v}, message="5 Actor")
215pattern define_actor_vehicleWidth(v:Vehicle) {
216 Vehicle.placedOn(v, lane);
217 Lane_Vertical(lane);
218 Vehicle.width(v, w);
219 check(w != 2.0);
220} or {
221 Vehicle.placedOn(v, lane);
222 Lane_Horizontal(lane);
223 Vehicle.width(v, w);
224 check(w != 3.0);
225}
226
227/////////actor-width (6)
228@Constraint(severity="error", key={v}, message="6 Actor")
229pattern define_actor_vehicleLength(v:Vehicle) {
230 Vehicle.placedOn(v, lane);
231 Lane_Vertical(lane);
232 Vehicle.length(v, l);
233 check(l != 3.0);
234} or {
235 Vehicle.placedOn(v, lane);
236 Lane_Horizontal(lane);
237 Vehicle.length(v, l);
238 check(l != 2.0);
239}
240
241/////----------------
242/////DERIVED FEATURES
243/////----------------
244/*
245@QueryBasedFeature
246pattern dist_near(a1: Actor, a2: Actor) {
247 find helper_getCoords(a1, a2, x1, x2, y1, y2);
248
249 //check(dx^2 + dy^2 < 10^2)
250 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10);
251 Actor.dist_near(a1, a2);
252}
253
254@QueryBasedFeature
255pattern dist_med(a1: Actor, a2: Actor) {
256 find helper_getCoords(a1, a2, x1, x2, y1, y2);
257
258 //check(10^2 < dx^2 + dy^2 < 15^2)
259 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10);
260 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15);
261 Actor.dist_med(a1, a2);
262}
263
264@QueryBasedFeature
265pattern dist_far(a1: Actor, a2: Actor) {
266 find helper_getCoords(a1, a2, x1, x2, y1, y2);
267
268 //check(dx^2 + dy^2 > 20^2)
269 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 20*20);
270 Actor.dist_far(a1, a2);
271}
272*/
273///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
274//Relation
275///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
276
277//@Constraint(severity="error", key={a1, a2}, message="1 Relation")
278//pattern define_relation_noSelfRelation(a1:Actor, a2:Actor) {
279// Relation.source(r, a1);
280// Relation.target(r, a2);
281// a1 == a2;
282//}
283
284//TODO do above but transitively?/
285//////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
286//CollisionExists
287///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
288
289
290//<<QUALTATIF ABSTRACTION>>
291/*
292@Constraint(severity="error", key={a1, a2}, message="x")
293pattern collisionExists_qualAbstr(a1:Actor, a2:Actor) {
294 CollisionExists.source(ce, a1);
295 CollisionExists.target(ce, a2);
296 Actor.placedOn(a1, vl1);
297 Lane_Vertical(vl1);
298 Actor.placedOn(a2, vl2);
299 Lane_Vertical(vl2);
300} or {
301 CollisionExists.source(ce, a1);
302 CollisionExists.target(ce, a2);
303 Actor.placedOn(a1, hl1);
304 Lane_Horizontal(hl1);
305 Actor.placedOn(a2, hl2);
306 Lane_Horizontal(hl2);
307}
308*/
309//<<END TEMP QUALITATIF ABSTRACTION>>
310
311
312////
313//CollisionExists - Time
314////
315
316
317@Constraint(severity="error", key={c}, message="x")
318pattern collisionExists_timeWithinBound(ss:CrossingScenario, c:CollisionExists) {
319 CrossingScenario.relations(ss, c);
320 CrossingScenario.maxTime(ss, maxTime);
321 CollisionExists.collisionTime(c, cTime);
322 check(cTime >= maxTime);}
323
324@Constraint(severity="error", key={c}, message="x")
325pattern collisionExists_timeNotNegative(c:CollisionExists) {
326 CollisionExists. collisionTime(c, cTime);
327 check(cTime <= 0.0);}
328
329////
330//CollisionExists - Physical Positioniung
331////
332
333private pattern helper_getCollExistsTime(a1:Actor, a2: Actor, cTime:java Double) {
334 CollisionExists.source(c, a1);
335 CollisionExists.target(c, a2);
336 CollisionExists. collisionTime(c, cTime);
337}
338
339private pattern helper_getYCoords(a:Actor, l:java Double,
340 yPos:java Double, ySpeed:java Double) {
341
342 Actor.length(a, l);
343 Actor.yPos(a, yPos);
344 Actor.ySpeed(a, ySpeed);
345}
346
347private pattern helper_getAllYCoords(a1:Actor, a2: Actor,
348 l1:java Double, l2:java Double, yPos1:java Double, yPos2:java Double,
349 ySpeed1:java Double, ySpeed2:java Double) {
350
351 CollisionExists.source(c, a1);
352 CollisionExists.target(c, a2);
353 find helper_getYCoords(a1, l1, yPos1, ySpeed1);
354 find helper_getYCoords(a2, l2, yPos2, ySpeed2);
355}
356
357private pattern helper_getXCoords(a:Actor, w:java Double,
358 xPos:java Double, xSpeed:java Double) {
359
360 Actor.width(a, w);
361 Actor.xPos(a, xPos);
362 Actor.xSpeed(a, xSpeed);
363}
364
365private pattern helper_getAllXCoords(a1:Actor, a2: Actor,
366 w1:java Double, w2:java Double, xPos1:java Double, xPos2:java Double,
367 xSpeed1:java Double, xSpeed2:java Double) {
368
369 CollisionExists.source(c, a1);
370 CollisionExists.target(c, a2);
371 find helper_getXCoords(a1, w1, xPos1, xSpeed1);
372 find helper_getXCoords(a2, w2, xPos2, xSpeed2);
373}
374
375@Constraint(severity="error", key={a1}, message="x")
376pattern collisionExists_defineCollision_y1(a1:Actor, a2:Actor) {
377
378 find helper_getCollExistsTime(a1, a2, cTime);
379 find helper_getAllYCoords(a1, a2, l1, l2, yPos1, yPos2, ySpeed1, ySpeed2);
380
381 //check(y_1_bottom > y_2_top
382 check((yPos1 + (ySpeed1 * cTime)) - (l1/2) > (yPos2 + (ySpeed2 * cTime)) + (l2/2));
383}
384
385@Constraint(severity="error", key={a1}, message="x")
386pattern collisionExists_defineCollision_y2(a1:Actor, a2:Actor) {
387 //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
388
389 find helper_getCollExistsTime(a1, a2, cTime);
390 find helper_getAllYCoords(a1, a2, l1, l2, yPos1, yPos2, ySpeed1, ySpeed2);
391
392 //check(y_1_top < y_2_bottom)
393 check((yPos1 + (ySpeed1 * cTime)) + (l1/2) < (yPos2 + (ySpeed2 * cTime)) - (l2/2));
394}
395
396@Constraint(severity="error", key={a1}, message="x")
397pattern collisionExists_defineCollision_x1(a1:Actor, a2:Actor) {
398
399 find helper_getCollExistsTime(a1, a2, cTime);
400 find helper_getAllXCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2);
401
402 //check(x_1_left > x_2_right)
403 check((xPos1 + (xSpeed1 * cTime)) - (w1/2) > (xPos2 + (xSpeed2 * cTime)) + (w2/2));
404}
405
406@Constraint(severity="error", key={a1}, message="x")
407pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor) {
408 //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
409
410 find helper_getCollExistsTime(a1, a2, cTime);
411 find helper_getAllXCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2);
412
413 //check(x_1_right < x_2_left)
414 check((xPos1 + (xSpeed1 * cTime)) + (w1/2) < (xPos2 + (xSpeed2 * cTime)) - (w2/2));
415}
416
417
418///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
419//VisionBlocked
420///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
421
422//<<QUALTATIF ABSTRACTION>>
423/*
424@Constraint(severity="error", key={a1, a2}, message="on 3 different lanes")
425pattern visionBlocked_qualAbstr(a1:Actor, a2:Actor) {
426 VisionBlocked.source(vb, a1);
427 VisionBlocked.target(vb, a2);
428 Actor.placedOn(a1, l);
429 Actor.placedOn(a2, l);
430} or {
431 VisionBlocked.source(vb, a1);
432 VisionBlocked.blockedBy(vb, a2);
433 Actor.placedOn(a1, l);
434 Actor.placedOn(a2, l);
435} or {
436 VisionBlocked.blockedBy(vb, a1);
437 VisionBlocked.target(vb, a2);
438 Actor.placedOn(a1, l);
439 Actor.placedOn(a2, l);
440}
441*/
442/*
443@Constraint(severity="error", key={a1, a2}, message="on lanes with different orientation")
444pattern visionBlocked_qualAbstr2(a1:Actor, a2:Actor) {
445 VisionBlocked.source(ce, a1);
446 VisionBlocked.target(ce, a2);
447 Actor.placedOn(a1, vl1);
448 Lane_Vertical(vl1);
449 Actor.placedOn(a2, vl2);
450 Lane_Vertical(vl2);
451} or {
452 VisionBlocked.source(ce, a1);
453 VisionBlocked.target(ce, a2);
454 Actor.placedOn(a1, hl1);
455 Lane_Horizontal(hl1);
456 Actor.placedOn(a2, hl2);
457 Lane_Horizontal(hl2);
458}
459*/
460
461////////////ADDED
462//to make decision for ITE
463//NOT NEEDED
464/*
465@Constraint(severity="error", key={a}, message="5 Actor")
466pattern define_vb_blvssrc(a:Actor) {
467 VisionBlocked.source(vb, a);
468 VisionBlocked.blockedBy(vb, b);
469 Actor.placedOn(a, lane);
470 Lane_Vertical(lane);
471 Actor.yPos(a, yPa);
472 Actor.yPos(b, yPb);
473 check(yPb <= yPa);
474} or {
475 VisionBlocked.source(vb, a);
476 VisionBlocked.blockedBy(vb, b);
477 Actor.placedOn(a, lane);
478 Lane_Horizontal(lane);
479 Actor.xPos(a, xPa);
480 Actor.xPos(a, xPb);
481 check(xPb <= xPa);
482}
483*/
484////////////ADDED
485//<<END QUALITATIF ABSTRACTION>>
486
487@Constraint(severity="error", key={a1, a2}, message="x")
488pattern visionBlocked_invalidBlocker(a1:Actor, a2:Actor) {
489 VisionBlocked.source(vb, a1);
490 VisionBlocked.target(vb, a2);
491 VisionBlocked.blockedBy(vb, a2);
492} or {
493 VisionBlocked.source(vb, a1);
494 VisionBlocked.target(vb, a2);
495 VisionBlocked.blockedBy(vb, a1);
496}
497
498@Constraint(severity="error", key={a1, vb}, message="x")
499pattern visionBlocked_ites_notOnSameVertLine(a1:Actor, a2:Actor, vb:VisionBlocked) {
500 //REQUIRED to avoid division by 0 in next 2 queries
501 VisionBlocked.source(vb, a1);
502 VisionBlocked.target(vb, a2);
503
504 Actor.xPos(a1, x1);
505 Actor.xPos(a2, x2);
506
507 //check(slope of a1-to-BlockerTop < slope of a1-to-a2)
508 check(x1 == x2);
509}
510
511private pattern helper_VB_getAllCoords(a1:Actor, a2: Actor,
512 x1:java Double, y1:java Double,
513 x2:java Double, y2:java Double,
514 xBlocker:java Double, yBlocker:java Double,
515 lenBlocker:java Double, widBlocker:java Double) {
516
517 VisionBlocked.source(vb, a1);
518 VisionBlocked.target(vb, a2);
519 VisionBlocked.blockedBy(vb, aBlocker);
520
521 Actor.xPos(a1, x1);
522 Actor.yPos(a1, y1);
523 Actor.xPos(a2, x2);
524 Actor.yPos(a2, y2);
525 Actor.xPos(aBlocker, xBlocker);
526 Actor.yPos(aBlocker, yBlocker);
527 Actor.length(aBlocker, lenBlocker);
528 Actor.width(aBlocker, widBlocker);
529}
530
531@Constraint(severity="error", key={a1}, message="x")
532pattern visionBlocked_ites_top(a1:Actor, a2:Actor) {
533
534 find helper_VB_getAllCoords(a1, a2,
535 x1, y1, x2, y2, xBlocker, yBlocker, lenBlocker, widBlocker);
536
537 //check(slope of a1-to-BlockerTop < slope of a1-to-a2)
538 check(
539 ( yBlocker - y1 + (if(xBlocker > x1){lenBlocker/2}else{0-lenBlocker/2})) /
540 ( xBlocker - x1 + (if(yBlocker > y1){0-widBlocker/2}else{widBlocker/2}))
541 < ((y1-y2)/(x1-x2)));
542}
543
544
545@Constraint(severity="error", key={a1}, message="x")
546pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor) {
547
548 find helper_VB_getAllCoords(a1, a2,
549 x1, y1, x2, y2, xBlocker, yBlocker, lenBlocker, widBlocker);
550
551 //check(slope of a1-to-BlockerBottom > slope of a1-to-a2)
552 check(
553 ( yBlocker - y1 + (if(xBlocker > x1){0-lenBlocker/2}else{lenBlocker/2})) /
554 ( xBlocker - x1 + (if(yBlocker > y1){widBlocker/2}else{0-widBlocker/2}))
555 > ((y1-y2)/(x1-x2)));
556}
557
558///////
559//BLOCKER IN BETWEEN
560///////
561
562private pattern helper_VB_getJustCoords(a1:Actor, a2: Actor,
563 x1:java Double, y1:java Double,
564 x2:java Double, y2:java Double,
565 xBlocker:java Double, yBlocker:java Double) {
566
567 VisionBlocked.source(vb, a1);
568 VisionBlocked.target(vb, a2);
569 VisionBlocked.blockedBy(vb, aBlocker);
570
571 Actor.xPos(a1, x1);
572 Actor.yPos(a1, y1);
573 Actor.xPos(a2, x2);
574 Actor.yPos(a2, y2);
575 Actor.xPos(aBlocker, xBlocker);
576 Actor.yPos(aBlocker, yBlocker);
577}
578
579/*
580//INFO may use approximation instead
581@Constraint(severity="error", key={a1}, message="x")
582pattern visionBlocked_xdistBSlargerThanxdistTS(a1:Actor, a2:Actor) {
583
584 find helper_VB_getJustCoords(a1, a2,
585 x1, y1, x2, y2, xBlocker, yBlocker);
586
587 //check(dist(A1, ABlocker) > dist(A1, A2))
588 check((x1-xBlocker)*(x1-xBlocker) + (y1-yBlocker)*(y1-yBlocker) > (x1-x2)*(x1-x2) + (y1-y2)*(y1-y2));
589}
590
591//INFO may use approximation instead
592@Constraint(severity="error", key={a1}, message="x")
593pattern visionBlocked_xdistBTlargerThanxdistST(a1:Actor, a2:Actor) {
594
595 find helper_VB_getJustCoords(a1, a2,
596 x1, y1, x2, y2, xBlocker, yBlocker);
597
598 //check(dist(A2, ABlocker) > dist(A2, A1))
599 check((x2-xBlocker)*(x2-xBlocker) + (y2-yBlocker)*(y2-yBlocker) > (x2-x1)*(x2-x1) + (y2-y1)*(y2-y1));
600}
601*/
602
603//INFO may use approximation instead
604@Constraint(severity="error", key={a1}, message="x")
605pattern visionBlocked_xdistBSlargerThanxdistTS(a1:Actor, a2:Actor) {
606
607 find helper_VB_getJustCoords(a1, a2,
608 x1, _, x2, _, xBlocker, _);
609
610 //check(dist(A1, ABlocker) > dist(A1, A2))
611 check((x1-xBlocker)*(x1-xBlocker) > (x1-x2)*(x1-x2));
612}
613
614//INFO may use approximation instead
615@Constraint(severity="error", key={a1}, message="x")
616pattern visionBlocked_xdistBTlargerThanxdistST(a1:Actor, a2:Actor) {
617
618 find helper_VB_getJustCoords(a1, a2,
619 x1, _, x2, _, xBlocker, _);
620
621 //check(dist(A2, ABlocker) > dist(A2, A1))
622 check((x2-xBlocker)*(x2-xBlocker) > (x2-x1)*(x2-x1));
623}
624
625//INFO may use approximation instead
626@Constraint(severity="error", key={a1}, message="x")
627pattern visionBlocked_ydistBSlargerThanydistTS(a1:Actor, a2:Actor) {
628
629 find helper_VB_getJustCoords(a1, a2,
630 _, y1, _, y2, _, yBlocker);
631
632 //check(dist(A1, ABlocker) > dist(A1, A2))
633 check((y1-yBlocker)*(y1-yBlocker) > (y1-y2)*(y1-y2));
634}
635
636//INFO may use approximation instead
637@Constraint(severity="error", key={a1}, message="x")
638pattern visionBlocked_ydistBTlargerThanydistST(a1:Actor, a2:Actor) {
639
640 find helper_VB_getJustCoords(a1, a2,
641 _, y1, _, y2, _, yBlocker);
642
643 //check(dist(A2, ABlocker) > dist(A2, A1))
644 check((y2-yBlocker)*(y2-yBlocker) > (y2-y1)*(y2-y1));
645}
646
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategyHints.vql b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategyHints.vql
new file mode 100644
index 00000000..6a9f106c
--- /dev/null
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategyHints.vql
@@ -0,0 +1,646 @@
1package queries
2
3import "http://www.example.com/crossingScenario"
4import "http://www.eclipse.org/emf/2002/Ecore"
5
6///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
7//Lane+Actor
8///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
9
10/////////Actor (a) on vertical lane (l) must have a.xPos=[l.rc, l.rc + l.nw]
11@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes")
12pattern define_placedOn_actorOnVerticalLane(a : Actor, vl:Lane_Vertical) {
13 Actor.placedOn(a, vl);
14 Actor.xPos(a, x);
15 Lane.referenceCoord(vl, r);
16 check(x <= r);
17} or {
18 Actor.placedOn(a, vl);
19 Actor.xPos(a, x);
20 Lane.referenceCoord(vl, r);
21// //<<<<OLD>>>>
22// Lane.numWidth(vl, w);
23// check(x >= (r + w));
24
25 //<<<<NEW>>>>: lanes all have width=3
26 check(x >= (r + 3.0));
27}
28
29@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes")
30pattern define_placedOn_actorOnHorizLane(a : Actor, hl:Lane_Horizontal) {
31 Actor.placedOn(a, hl);
32 Actor.yPos(a, y);
33 Lane.referenceCoord(hl, r);
34 check(y <= r);
35} or {
36 Actor.placedOn(a, hl);
37 Actor.yPos(a, y);
38 Lane.referenceCoord(hl, r);
39// //<<OLD>>
40// Lane.numWidth(hl, w);
41// check(y >= (r + w));
42
43 //<<NEW>>: lanes all have width=3
44 check(y >= (r + 3.0));
45
46}
47
48///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
49//Actor
50///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
51
52/////----------------
53//Xpos and Ypos Bounds
54/////----------------
55
56private pattern helper_horiz_getXAndBounds(cs:CrossingScenario, a:Actor,
57 xMax:java Double, xP:java Double) {
58 Actor.placedOn(a, hl);
59 Lane_Horizontal(hl);
60 CrossingScenario.actors(cs, a);
61 CrossingScenario.xSize(cs, xMax);
62 Actor.xPos(a, xP);
63}
64
65private pattern helper_vert_getYAndBounds(cs:CrossingScenario, a:Actor,
66 yMax:java Double, yP:java Double) {
67 Actor.placedOn(a, vl);
68 Lane_Vertical(vl);
69 CrossingScenario.actors(cs, a);
70 CrossingScenario.ySize(cs, yMax);
71 Actor.yPos(a, yP);
72}
73
74@Constraint(severity="error", key={cs}, message="x")
75pattern define_actor_maxXp(cs:CrossingScenario, a:Actor) {
76 find helper_horiz_getXAndBounds(cs, a, xMax, xP);
77 check(xP >= xMax);}
78
79@Constraint(severity="error", key={cs}, message="x")
80pattern define_actor_minXp(cs:CrossingScenario, a:Actor) {
81 find helper_horiz_getXAndBounds(cs, a, xMax, xP);
82 check(xP <= 0-xMax);}
83
84@Constraint(severity="error", key={cs}, message="x")
85pattern define_actor_maxYp(cs:CrossingScenario, a:Actor) {
86 find helper_vert_getYAndBounds(cs, a, yMax, yP);
87 check(yP >= yMax);}
88
89@Constraint(severity="error", key={cs}, message="x")
90pattern define_actor_minYp(cs:CrossingScenario, a:Actor) {
91 find helper_vert_getYAndBounds(cs, a, yMax, yP);
92 check(yP <= 0-yMax);}
93
94////////////ADDED
95//to reduce overlap
96//NEEDED
97
98@Constraint(severity="error", key={a}, message="5 Actor")
99pattern define_actor_wrtLane(a:Actor) {
100 Actor.placedOn(a, lane);
101 Lane_Vertical(lane);
102 Actor.yPos(a, yP);
103 check(yP > 0.0-1.0);
104} or {
105 Actor.placedOn(a, lane);
106 Lane_Horizontal(lane);
107 Actor.xPos(a, xP);
108 check(xP > 0.0-1.0);
109}
110
111////////////ADDED
112
113//Minimum Distances
114private pattern helper_getCoords(a1:Actor,
115 a2: Actor, x1:java Double, x2:java Double, y1:java Double, y2:java Double) {
116 Actor.xPos(a1, x1);
117 Actor.yPos(a1, y1);
118 Actor.xPos(a2, x2);
119 Actor.yPos(a2, y2);
120}
121
122//INFO may remove?
123@Constraint(severity="error", key={a1, a2}, message="x")
124pattern define_actor_minimumDistance(a1: Actor, a2: Actor) {
125 find helper_getCoords(a1, a2, x1, x2, y1, y2);
126 a1 != a2;
127 //check(dx^2 + dy^2 < 3^2)
128 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 3*3);
129}
130
131/////----------------
132//Xspeed and Yspeed bounds
133/////----------------
134
135/////////VERTICAL LANE
136@Constraint(severity="error", key={a}, message="7 Actor")
137pattern define_actor_actorOnVertLaneHasxSpeed0(a:Actor) {
138 Actor.placedOn(a, vl);
139 Lane_Vertical(vl);
140 Actor.xSpeed(a, xSpeed);
141 check(xSpeed != 0.0);
142}
143
144private pattern helper_vert_getYSpeedAndBounds(cs:CrossingScenario, a:Actor,
145 ySpeedMax:java Double, ySpeed:java Double) {
146 Actor.placedOn(a, vl);
147 Lane_Vertical(vl);
148 CrossingScenario.actors(cs, a);
149 CrossingScenario.maxYSpeed(cs, ySpeedMax);
150 Actor.ySpeed(a, ySpeed);
151}
152
153@Constraint(severity="error", key={cs}, message="x")
154pattern define_actor_actorOnVertLaneMinYs(cs:CrossingScenario, a:Actor) {
155 find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS);
156 check(yS <= 0.0-ySMax);
157}
158
159@Constraint(severity="error", key={cs}, message="x")
160pattern define_actor_actorOnVertLaneMaxYs(cs:CrossingScenario, a:Actor) {
161 find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS);
162 check(yS >= ySMax);
163}
164
165/////////HORIZONTAL LANE
166@Constraint(severity="error", key={a}, message="7 Actor")
167pattern define_actor_actorOnHorizLaneHasySpeed0(a:Actor) {
168 Actor.placedOn(a, hl);
169 Lane_Horizontal(hl);
170 Actor.ySpeed(a, ySpeed);
171 check(ySpeed != 0.0);
172}
173
174private pattern helper_horiz_getXSpeedAndBounds(cs:CrossingScenario, a:Actor,
175 xSpeedMax:java Double, xSpeed:java Double) {
176 Actor.placedOn(a, hl);
177 Lane_Horizontal(hl);
178 CrossingScenario.actors(cs, a);
179 CrossingScenario.maxXSpeed(cs, xSpeedMax);
180 Actor.xSpeed(a, xSpeed);
181}
182
183@Constraint(severity="error", key={cs}, message="x")
184pattern define_actor_actorOnHorizLaneMinXs(cs:CrossingScenario, a:Actor) {
185 find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS);
186 check(xS <= 0.0-xSMax);
187}
188
189@Constraint(severity="error", key={cs}, message="x")
190pattern define_actor_actorOnHorizLaneMaxXs(cs:CrossingScenario, a:Actor) {
191 find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS);
192 check(xS >= xSMax);
193}
194
195/////----------------
196/////WIDTH and LENGTH
197/////----------------
198
199///////pedestrian-width (3)
200@Constraint(severity="error", key={p}, message="3 Actor")
201pattern define_actor_pedestrianWidth(p:Pedestrian) {
202 Pedestrian.width(p, w);
203 check(w != 1.0);
204}
205
206/////////pedestrian-width (4)
207@Constraint(severity="error", key={p}, message="4 Actor")
208pattern define_actor_pedestrianLength(p:Pedestrian) {
209 Pedestrian.length(p, l);
210 check(l != 1.0);
211}
212
213/////////actor-width (5)
214@Constraint(severity="error", key={v}, message="5 Actor")
215pattern define_actor_vehicleWidth(v:Vehicle) {
216 Vehicle.placedOn(v, lane);
217 Lane_Vertical(lane);
218 Vehicle.width(v, w);
219 check(w != 2.0);
220} or {
221 Vehicle.placedOn(v, lane);
222 Lane_Horizontal(lane);
223 Vehicle.width(v, w);
224 check(w != 3.0);
225}
226
227/////////actor-width (6)
228@Constraint(severity="error", key={v}, message="6 Actor")
229pattern define_actor_vehicleLength(v:Vehicle) {
230 Vehicle.placedOn(v, lane);
231 Lane_Vertical(lane);
232 Vehicle.length(v, l);
233 check(l != 3.0);
234} or {
235 Vehicle.placedOn(v, lane);
236 Lane_Horizontal(lane);
237 Vehicle.length(v, l);
238 check(l != 2.0);
239}
240
241/////----------------
242/////DERIVED FEATURES
243/////----------------
244/*
245@QueryBasedFeature
246pattern dist_near(a1: Actor, a2: Actor) {
247 find helper_getCoords(a1, a2, x1, x2, y1, y2);
248
249 //check(dx^2 + dy^2 < 10^2)
250 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10);
251 Actor.dist_near(a1, a2);
252}
253
254@QueryBasedFeature
255pattern dist_med(a1: Actor, a2: Actor) {
256 find helper_getCoords(a1, a2, x1, x2, y1, y2);
257
258 //check(10^2 < dx^2 + dy^2 < 15^2)
259 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10);
260 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15);
261 Actor.dist_med(a1, a2);
262}
263
264@QueryBasedFeature
265pattern dist_far(a1: Actor, a2: Actor) {
266 find helper_getCoords(a1, a2, x1, x2, y1, y2);
267
268 //check(dx^2 + dy^2 > 20^2)
269 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 20*20);
270 Actor.dist_far(a1, a2);
271}
272*/
273///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
274//Relation
275///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
276
277//@Constraint(severity="error", key={a1, a2}, message="1 Relation")
278//pattern define_relation_noSelfRelation(a1:Actor, a2:Actor) {
279// Relation.source(r, a1);
280// Relation.target(r, a2);
281// a1 == a2;
282//}
283
284//TODO do above but transitively?/
285//////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
286//CollisionExists
287///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
288
289
290//<<QUALTATIF ABSTRACTION>>
291
292@Constraint(severity="error", key={a1, a2}, message="x")
293pattern collisionExists_qualAbstr(a1:Actor, a2:Actor) {
294 CollisionExists.source(ce, a1);
295 CollisionExists.target(ce, a2);
296 Actor.placedOn(a1, vl1);
297 Lane_Vertical(vl1);
298 Actor.placedOn(a2, vl2);
299 Lane_Vertical(vl2);
300} or {
301 CollisionExists.source(ce, a1);
302 CollisionExists.target(ce, a2);
303 Actor.placedOn(a1, hl1);
304 Lane_Horizontal(hl1);
305 Actor.placedOn(a2, hl2);
306 Lane_Horizontal(hl2);
307}
308
309//<<END TEMP QUALITATIF ABSTRACTION>>
310
311
312////
313//CollisionExists - Time
314////
315
316
317@Constraint(severity="error", key={c}, message="x")
318pattern collisionExists_timeWithinBound(ss:CrossingScenario, c:CollisionExists) {
319 CrossingScenario.relations(ss, c);
320 CrossingScenario.maxTime(ss, maxTime);
321 CollisionExists.collisionTime(c, cTime);
322 check(cTime >= maxTime);}
323
324@Constraint(severity="error", key={c}, message="x")
325pattern collisionExists_timeNotNegative(c:CollisionExists) {
326 CollisionExists. collisionTime(c, cTime);
327 check(cTime <= 0.0);}
328
329////
330//CollisionExists - Physical Positioniung
331////
332
333private pattern helper_getCollExistsTime(a1:Actor, a2: Actor, cTime:java Double) {
334 CollisionExists.source(c, a1);
335 CollisionExists.target(c, a2);
336 CollisionExists. collisionTime(c, cTime);
337}
338
339private pattern helper_getYCoords(a:Actor, l:java Double,
340 yPos:java Double, ySpeed:java Double) {
341
342 Actor.length(a, l);
343 Actor.yPos(a, yPos);
344 Actor.ySpeed(a, ySpeed);
345}
346
347private pattern helper_getAllYCoords(a1:Actor, a2: Actor,
348 l1:java Double, l2:java Double, yPos1:java Double, yPos2:java Double,
349 ySpeed1:java Double, ySpeed2:java Double) {
350
351 CollisionExists.source(c, a1);
352 CollisionExists.target(c, a2);
353 find helper_getYCoords(a1, l1, yPos1, ySpeed1);
354 find helper_getYCoords(a2, l2, yPos2, ySpeed2);
355}
356
357private pattern helper_getXCoords(a:Actor, w:java Double,
358 xPos:java Double, xSpeed:java Double) {
359
360 Actor.width(a, w);
361 Actor.xPos(a, xPos);
362 Actor.xSpeed(a, xSpeed);
363}
364
365private pattern helper_getAllXCoords(a1:Actor, a2: Actor,
366 w1:java Double, w2:java Double, xPos1:java Double, xPos2:java Double,
367 xSpeed1:java Double, xSpeed2:java Double) {
368
369 CollisionExists.source(c, a1);
370 CollisionExists.target(c, a2);
371 find helper_getXCoords(a1, w1, xPos1, xSpeed1);
372 find helper_getXCoords(a2, w2, xPos2, xSpeed2);
373}
374
375@Constraint(severity="error", key={a1}, message="x")
376pattern collisionExists_defineCollision_y1(a1:Actor, a2:Actor) {
377
378 find helper_getCollExistsTime(a1, a2, cTime);
379 find helper_getAllYCoords(a1, a2, l1, l2, yPos1, yPos2, ySpeed1, ySpeed2);
380
381 //check(y_1_bottom > y_2_top
382 check((yPos1 + (ySpeed1 * cTime)) - (l1/2) > (yPos2 + (ySpeed2 * cTime)) + (l2/2));
383}
384
385@Constraint(severity="error", key={a1}, message="x")
386pattern collisionExists_defineCollision_y2(a1:Actor, a2:Actor) {
387 //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
388
389 find helper_getCollExistsTime(a1, a2, cTime);
390 find helper_getAllYCoords(a1, a2, l1, l2, yPos1, yPos2, ySpeed1, ySpeed2);
391
392 //check(y_1_top < y_2_bottom)
393 check((yPos1 + (ySpeed1 * cTime)) + (l1/2) < (yPos2 + (ySpeed2 * cTime)) - (l2/2));
394}
395
396@Constraint(severity="error", key={a1}, message="x")
397pattern collisionExists_defineCollision_x1(a1:Actor, a2:Actor) {
398
399 find helper_getCollExistsTime(a1, a2, cTime);
400 find helper_getAllXCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2);
401
402 //check(x_1_left > x_2_right)
403 check((xPos1 + (xSpeed1 * cTime)) - (w1/2) > (xPos2 + (xSpeed2 * cTime)) + (w2/2));
404}
405
406@Constraint(severity="error", key={a1}, message="x")
407pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor) {
408 //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
409
410 find helper_getCollExistsTime(a1, a2, cTime);
411 find helper_getAllXCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2);
412
413 //check(x_1_right < x_2_left)
414 check((xPos1 + (xSpeed1 * cTime)) + (w1/2) < (xPos2 + (xSpeed2 * cTime)) - (w2/2));
415}
416
417
418///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
419//VisionBlocked
420///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
421
422//<<QUALTATIF ABSTRACTION>>
423/*
424@Constraint(severity="error", key={a1, a2}, message="on 3 different lanes")
425pattern visionBlocked_qualAbstr(a1:Actor, a2:Actor) {
426 VisionBlocked.source(vb, a1);
427 VisionBlocked.target(vb, a2);
428 Actor.placedOn(a1, l);
429 Actor.placedOn(a2, l);
430} or {
431 VisionBlocked.source(vb, a1);
432 VisionBlocked.blockedBy(vb, a2);
433 Actor.placedOn(a1, l);
434 Actor.placedOn(a2, l);
435} or {
436 VisionBlocked.blockedBy(vb, a1);
437 VisionBlocked.target(vb, a2);
438 Actor.placedOn(a1, l);
439 Actor.placedOn(a2, l);
440}
441*/
442
443@Constraint(severity="error", key={a1, a2}, message="on lanes with different orientation")
444pattern visionBlocked_qualAbstr2(a1:Actor, a2:Actor) {
445 VisionBlocked.source(ce, a1);
446 VisionBlocked.target(ce, a2);
447 Actor.placedOn(a1, vl1);
448 Lane_Vertical(vl1);
449 Actor.placedOn(a2, vl2);
450 Lane_Vertical(vl2);
451} or {
452 VisionBlocked.source(ce, a1);
453 VisionBlocked.target(ce, a2);
454 Actor.placedOn(a1, hl1);
455 Lane_Horizontal(hl1);
456 Actor.placedOn(a2, hl2);
457 Lane_Horizontal(hl2);
458}
459
460
461////////////ADDED
462//to make decision for ITE
463//NOT NEEDED
464/*
465@Constraint(severity="error", key={a}, message="5 Actor")
466pattern define_vb_blvssrc(a:Actor) {
467 VisionBlocked.source(vb, a);
468 VisionBlocked.blockedBy(vb, b);
469 Actor.placedOn(a, lane);
470 Lane_Vertical(lane);
471 Actor.yPos(a, yPa);
472 Actor.yPos(b, yPb);
473 check(yPb <= yPa);
474} or {
475 VisionBlocked.source(vb, a);
476 VisionBlocked.blockedBy(vb, b);
477 Actor.placedOn(a, lane);
478 Lane_Horizontal(lane);
479 Actor.xPos(a, xPa);
480 Actor.xPos(a, xPb);
481 check(xPb <= xPa);
482}
483*/
484////////////ADDED
485//<<END QUALITATIF ABSTRACTION>>
486
487@Constraint(severity="error", key={a1, a2}, message="x")
488pattern visionBlocked_invalidBlocker(a1:Actor, a2:Actor) {
489 VisionBlocked.source(vb, a1);
490 VisionBlocked.target(vb, a2);
491 VisionBlocked.blockedBy(vb, a2);
492} or {
493 VisionBlocked.source(vb, a1);
494 VisionBlocked.target(vb, a2);
495 VisionBlocked.blockedBy(vb, a1);
496}
497
498@Constraint(severity="error", key={a1, vb}, message="x")
499pattern visionBlocked_ites_notOnSameVertLine(a1:Actor, a2:Actor, vb:VisionBlocked) {
500 //REQUIRED to avoid division by 0 in next 2 queries
501 VisionBlocked.source(vb, a1);
502 VisionBlocked.target(vb, a2);
503
504 Actor.xPos(a1, x1);
505 Actor.xPos(a2, x2);
506
507 //check(slope of a1-to-BlockerTop < slope of a1-to-a2)
508 check(x1 == x2);
509}
510
511private pattern helper_VB_getAllCoords(a1:Actor, a2: Actor,
512 x1:java Double, y1:java Double,
513 x2:java Double, y2:java Double,
514 xBlocker:java Double, yBlocker:java Double,
515 lenBlocker:java Double, widBlocker:java Double) {
516
517 VisionBlocked.source(vb, a1);
518 VisionBlocked.target(vb, a2);
519 VisionBlocked.blockedBy(vb, aBlocker);
520
521 Actor.xPos(a1, x1);
522 Actor.yPos(a1, y1);
523 Actor.xPos(a2, x2);
524 Actor.yPos(a2, y2);
525 Actor.xPos(aBlocker, xBlocker);
526 Actor.yPos(aBlocker, yBlocker);
527 Actor.length(aBlocker, lenBlocker);
528 Actor.width(aBlocker, widBlocker);
529}
530
531@Constraint(severity="error", key={a1}, message="x")
532pattern visionBlocked_ites_top(a1:Actor, a2:Actor) {
533
534 find helper_VB_getAllCoords(a1, a2,
535 x1, y1, x2, y2, xBlocker, yBlocker, lenBlocker, widBlocker);
536
537 //check(slope of a1-to-BlockerTop < slope of a1-to-a2)
538 check(
539 ( yBlocker - y1 + (if(xBlocker > x1){lenBlocker/2}else{0-lenBlocker/2})) /
540 ( xBlocker - x1 + (if(yBlocker > y1){0-widBlocker/2}else{widBlocker/2}))
541 < ((y1-y2)/(x1-x2)));
542}
543
544
545@Constraint(severity="error", key={a1}, message="x")
546pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor) {
547
548 find helper_VB_getAllCoords(a1, a2,
549 x1, y1, x2, y2, xBlocker, yBlocker, lenBlocker, widBlocker);
550
551 //check(slope of a1-to-BlockerBottom > slope of a1-to-a2)
552 check(
553 ( yBlocker - y1 + (if(xBlocker > x1){0-lenBlocker/2}else{lenBlocker/2})) /
554 ( xBlocker - x1 + (if(yBlocker > y1){widBlocker/2}else{0-widBlocker/2}))
555 > ((y1-y2)/(x1-x2)));
556}
557
558///////
559//BLOCKER IN BETWEEN
560///////
561
562private pattern helper_VB_getJustCoords(a1:Actor, a2: Actor,
563 x1:java Double, y1:java Double,
564 x2:java Double, y2:java Double,
565 xBlocker:java Double, yBlocker:java Double) {
566
567 VisionBlocked.source(vb, a1);
568 VisionBlocked.target(vb, a2);
569 VisionBlocked.blockedBy(vb, aBlocker);
570
571 Actor.xPos(a1, x1);
572 Actor.yPos(a1, y1);
573 Actor.xPos(a2, x2);
574 Actor.yPos(a2, y2);
575 Actor.xPos(aBlocker, xBlocker);
576 Actor.yPos(aBlocker, yBlocker);
577}
578
579/*
580//INFO may use approximation instead
581@Constraint(severity="error", key={a1}, message="x")
582pattern visionBlocked_xdistBSlargerThanxdistTS(a1:Actor, a2:Actor) {
583
584 find helper_VB_getJustCoords(a1, a2,
585 x1, y1, x2, y2, xBlocker, yBlocker);
586
587 //check(dist(A1, ABlocker) > dist(A1, A2))
588 check((x1-xBlocker)*(x1-xBlocker) + (y1-yBlocker)*(y1-yBlocker) > (x1-x2)*(x1-x2) + (y1-y2)*(y1-y2));
589}
590
591//INFO may use approximation instead
592@Constraint(severity="error", key={a1}, message="x")
593pattern visionBlocked_xdistBTlargerThanxdistST(a1:Actor, a2:Actor) {
594
595 find helper_VB_getJustCoords(a1, a2,
596 x1, y1, x2, y2, xBlocker, yBlocker);
597
598 //check(dist(A2, ABlocker) > dist(A2, A1))
599 check((x2-xBlocker)*(x2-xBlocker) + (y2-yBlocker)*(y2-yBlocker) > (x2-x1)*(x2-x1) + (y2-y1)*(y2-y1));
600}
601*/
602
603//INFO may use approximation instead
604@Constraint(severity="error", key={a1}, message="x")
605pattern visionBlocked_xdistBSlargerThanxdistTS(a1:Actor, a2:Actor) {
606
607 find helper_VB_getJustCoords(a1, a2,
608 x1, _, x2, _, xBlocker, _);
609
610 //check(dist(A1, ABlocker) > dist(A1, A2))
611 check((x1-xBlocker)*(x1-xBlocker) > (x1-x2)*(x1-x2));
612}
613
614//INFO may use approximation instead
615@Constraint(severity="error", key={a1}, message="x")
616pattern visionBlocked_xdistBTlargerThanxdistST(a1:Actor, a2:Actor) {
617
618 find helper_VB_getJustCoords(a1, a2,
619 x1, _, x2, _, xBlocker, _);
620
621 //check(dist(A2, ABlocker) > dist(A2, A1))
622 check((x2-xBlocker)*(x2-xBlocker) > (x2-x1)*(x2-x1));
623}
624
625//INFO may use approximation instead
626@Constraint(severity="error", key={a1}, message="x")
627pattern visionBlocked_ydistBSlargerThanydistTS(a1:Actor, a2:Actor) {
628
629 find helper_VB_getJustCoords(a1, a2,
630 _, y1, _, y2, _, yBlocker);
631
632 //check(dist(A1, ABlocker) > dist(A1, A2))
633 check((y1-yBlocker)*(y1-yBlocker) > (y1-y2)*(y1-y2));
634}
635
636//INFO may use approximation instead
637@Constraint(severity="error", key={a1}, message="x")
638pattern visionBlocked_ydistBTlargerThanydistST(a1:Actor, a2:Actor) {
639
640 find helper_VB_getJustCoords(a1, a2,
641 _, y1, _, y2, _, yBlocker);
642
643 //check(dist(A2, ABlocker) > dist(A2, A1))
644 check((y2-yBlocker)*(y2-yBlocker) > (y2-y1)*(y2-y1));
645}
646
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runCrossScenario.sh b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runCrossScenario.sh
new file mode 100755
index 00000000..8a6a30be
--- /dev/null
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runCrossScenario.sh
@@ -0,0 +1,21 @@
1#!/usr/bin/bash
2NODE="$1"
3./run.sh "${NODE}" -d CrossScenario -lb 3 -nm 1 -nr 10 -rt 300 -ns z3 -drto 300000
4./run.sh "${NODE}" -d CrossScenario -lb 3 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000
5./run.sh "${NODE}" -d CrossScenario -lb 4 -nm 1 -nr 10 -rt 300 -ns z3 -drto 300000
6./run.sh "${NODE}" -d CrossScenario -lb 4 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000
7./run.sh "${NODE}" -d CrossScenario -lb 6 -nm 1 -nr 10 -rt 300 -ns z3 -drto 300000
8./run.sh "${NODE}" -d CrossScenario -lb 6 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000
9./run.sh "${NODE}" -d CrossScenario -lb 8 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000
10./run.sh "${NODE}" -d CrossScenario -lb 9 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000
11./run.sh "${NODE}" -d CrossScenario -lb 12 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000
12./run.sh "${NODE}" -d CrossScenario -lb 15 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000
13./run.sh "${NODE}" -d CrossScenario -lb 16 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000
14./run.sh "${NODE}" -d CrossScenario -lb 18 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000
15
16./run.sh "${NODE}" -d CrossScenario -lb 8 -nm 1 -nr 10 -rt 300 -ns z3 -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000
17./run.sh "${NODE}" -d CrossScenario -lb 20 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000
18
19./run.sh "${NODE}" -d CrossScenario -lb 21 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000
20./run.sh "${NODE}" -d CrossScenario -lb 9 -nm 1 -nr 10 -rt 300 -ns z3 -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000
21
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runCrossScenarioStrategy.sh b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runCrossScenarioStrategy.sh
new file mode 100755
index 00000000..5ceda582
--- /dev/null
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runCrossScenarioStrategy.sh
@@ -0,0 +1,15 @@
1#!/usr/bin/bash
2NODE="$1"
3./run.sh "${NODE}" -d StrategyYes -lb 0 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000
4
5./run.sh "${NODE}" -d StrategyNoWithHints -lb 1 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 10000
6./run.sh "${NODE}" -d StrategyNo -lb 1 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 10000
7
8./run.sh "${NODE}" -d StrategyNoWithHints -lb 1 -ub 1 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 10000
9./run.sh "${NODE}" -d StrategyNo -lb 1 -ub 1 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 10000
10
11./run.sh "${NODE}" -d StrategyNoWithHints -lb 0 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 10000
12./run.sh "${NODE}" -d StrategyNo -lb 0 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 10000
13
14./run.sh "${NODE}" -d StrategyNoWithHints -lb 0 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000
15./run.sh "${NODE}" -d StrategyNo -lb 0 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runTestCrossScenario.sh b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runTestCrossScenario.sh
new file mode 100755
index 00000000..64a72200
--- /dev/null
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runTestCrossScenario.sh
@@ -0,0 +1,11 @@
1#!/usr/bin/bash
2NODE="$1"
3
4./run.sh "${NODE}" -d CrossScenario -lb 3 -nm 1 -nr 1 -rt 300 -ns z3 -drto 300000
5./run.sh "${NODE}" -d CrossScenario -lb 3 -nm 1 -nr 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000
6
7./run.sh "${NODE}" -d CrossScenario -lb 300 -nm 1 -nr 1 -rt 10 -ns z3 -drto 2000
8./run.sh "${NODE}" -d CrossScenario -lb 300 -nm 1 -nr 1 -rt 10 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 2000
9
10./run.sh "${NODE}" -d StrategyYes -lb 0 -nr 1 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000
11./run.sh "${NODE}" -d StrategyNoWithHints -lb 1 -ub 1 -nr 1 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 10000 \ No newline at end of file
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend
index eddb8bb5..78d86504 100644
--- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend
@@ -39,6 +39,7 @@ class RunGeneratorConfig {
39 static var RUNTIME = 1500 39 static var RUNTIME = 1500
40 static var NUM_SOLVER = "z3" 40 static var NUM_SOLVER = "z3"
41 static var DREAL_PATH = "" 41 static var DREAL_PATH = ""
42 static var DREAL_TIMEOUT = "-2"
42// static var SCOPE_PROPAGATOR = "typeHierarchy" 43// static var SCOPE_PROPAGATOR = "typeHierarchy"
43 44
44 static var DOMAIN = "FamilyTree" // "FamilyTree", "Satellite", "Taxation" 45 static var DOMAIN = "FamilyTree" // "FamilyTree", "Satellite", "Taxation"
@@ -75,6 +76,9 @@ class RunGeneratorConfig {
75 val drp = new Option("drp", "drealPath", true, "path to dreal executeable") 76 val drp = new Option("drp", "drealPath", true, "path to dreal executeable")
76 options.addOption(drp) 77 options.addOption(drp)
77 78
79 val drto = new Option("drto", "drealTimeout", true, "drealTimeout")
80 options.addOption(drto)
81
78// val sp = new Option("sp", "scopePropagator", true, "scope Propagator") 82// val sp = new Option("sp", "scopePropagator", true, "scope Propagator")
79// options.addOption(sp) 83// options.addOption(sp)
80// 84//
@@ -82,7 +86,7 @@ class RunGeneratorConfig {
82 options.addOption(d) 86 options.addOption(d)
83 87
84 val hh = new Option("hh", "household", true, "number of households") 88 val hh = new Option("hh", "household", true, "number of households")
85 options.addOption(hh) 89 options.addOption(hh)
86 90
87 val CommandLineParser parser = new BasicParser 91 val CommandLineParser parser = new BasicParser
88 val formatter = new HelpFormatter() 92 val formatter = new HelpFormatter()
@@ -110,6 +114,8 @@ class RunGeneratorConfig {
110 if(nsIn !== null && nsIn.equals("dreal")) NUM_SOLVER = "dreal-local" 114 if(nsIn !== null && nsIn.equals("dreal")) NUM_SOLVER = "dreal-local"
111 val drpIn = cmd.getOptionValue("drealPath") 115 val drpIn = cmd.getOptionValue("drealPath")
112 if(drpIn !== null) DREAL_PATH = drpIn 116 if(drpIn !== null) DREAL_PATH = drpIn
117 val drtoIn = cmd.getOptionValue("drealTimeout")
118 if(drtoIn !== null) DREAL_TIMEOUT = drtoIn
113// val spIn = cmd.getOptionValue("scopePropagator") 119// val spIn = cmd.getOptionValue("scopePropagator")
114// if(spIn !== null ) SCOPE_PROPAGATOR = spIn 120// if(spIn !== null ) SCOPE_PROPAGATOR = spIn
115 val dIn = cmd.getOptionValue("domain") 121 val dIn = cmd.getOptionValue("domain")
@@ -136,14 +142,16 @@ class RunGeneratorConfig {
136 ", SIZE=" + SIZE_LB + "to" + SIZE_UB + 142 ", SIZE=" + SIZE_LB + "to" + SIZE_UB +
137 ", Runs=" + RUNS + 143 ", Runs=" + RUNS +
138 ", ModelsPerRun=" + MODELS + 144 ", ModelsPerRun=" + MODELS +
139 ", Runtime=" + RUNTIME + ">>") 145 ", Runtime=" + RUNTIME +
146 ", dreal-timeout=" + DREAL_TIMEOUT + ">>")
140 if (isTaxation) println("<<Households: " + HOUSEHOLD + ">>") 147 if (isTaxation) println("<<Households: " + HOUSEHOLD + ">>")
141 148
142 var naming = DOMAIN + "/size" + toStr(SIZE_LB) + "to" + toStr(SIZE_UB) + 149 var naming = DOMAIN + "/size" + toStr(SIZE_LB) + "to" + toStr(SIZE_UB) +
143 "r" + RUNS + 150 "r" + RUNS +
144 "n" + MODELS + 151 "n" + MODELS +
145 "rt" + RUNTIME + 152 "rt" + RUNTIME +
146 "ns" + NUM_SOLVER 153 "ns" + NUM_SOLVER +
154 "drto" + DREAL_TIMEOUT
147 if (isTaxation) naming = naming + "hh" + HOUSEHOLD 155 if (isTaxation) naming = naming + "hh" + HOUSEHOLD
148 val outputPath = "measurements/" + "models/" + naming + "_" + formattedDate 156 val outputPath = "measurements/" + "models/" + naming + "_" + formattedDate
149 val debugPath = "measurements/" + "debug/" + naming + "_" + formattedDate 157 val debugPath = "measurements/" + "debug/" + naming + "_" + formattedDate
@@ -211,6 +219,10 @@ class RunGeneratorConfig {
211 numSolverEntry.value = NUM_SOLVER 219 numSolverEntry.value = NUM_SOLVER
212 val drealPathEntry = configScope.entries.get(2) as CustomEntry 220 val drealPathEntry = configScope.entries.get(2) as CustomEntry
213 drealPathEntry.value = DREAL_PATH 221 drealPathEntry.value = DREAL_PATH
222 if (DREAL_TIMEOUT != "-2") {
223 val drealTimeoutEntry = configScope.entries.get(3) as CustomEntry
224 drealTimeoutEntry.value = DREAL_TIMEOUT
225 }
214// val scopePropEntry = configScope.entries.get(3) as CustomEntry 226// val scopePropEntry = configScope.entries.get(3) as CustomEntry
215// scopePropEntry.value = SCOPE_PROPAGATOR 227// scopePropEntry.value = SCOPE_PROPAGATOR
216 228
generated by cgit v1.2.3 (git 2.25.1) at 2024-04-20 15:10:02 +0000