Commit 39caeb15 authored by Ayoub Nouri's avatar Ayoub Nouri
Browse files

updated some test for ESROCOS report

parent bc21a984
......@@ -45,14 +45,81 @@ public class TestFormulaModel {
long startTime = System.currentTimeMillis();
test14();
test18();
long endTime = System.currentTimeMillis();
long totalTime = endTime - startTime;
System.out.println("Overall time : "+totalTime);
}
}
public static void test18(){
/** Building a test trace */
ArrayList<StateVariable> sv0 = new ArrayList<>();
sv0.add(new StateVariable("a", "true", "bool"));
sv0.add(new StateVariable("b", "false", "bool"));
sv0.add(new StateVariable("c", "false", "bool"));
State s0 = new State(sv0, 0.0);
ArrayList<StateVariable> sv1 = new ArrayList<>();
sv1.add(new StateVariable("a", "true", "bool"));
sv1.add(new StateVariable("b", "false", "bool"));
sv1.add(new StateVariable("c", "false", "bool"));
State s1 = new State(sv1, 1.0);
ArrayList<StateVariable> sv2 = new ArrayList<>();
sv2.add(new StateVariable("a", "false", "bool"));
sv2.add(new StateVariable("b", "true", "bool"));
sv2.add(new StateVariable("c", "false", "bool"));
//sv2.add(new StateVariable("b", "10", "int"));
State s2 = new State(sv2, 5.0);
ArrayList<StateVariable> sv3 = new ArrayList<>();
sv3.add(new StateVariable("a", "true", "bool"));
sv3.add(new StateVariable("b", "false", "bool"));
sv3.add(new StateVariable("c", "false", "bool"));
State s3 = new State(sv3, 6.0);
ArrayList<StateVariable> sv4 = new ArrayList<>();
sv4.add(new StateVariable("a", "false", "bool"));
sv4.add(new StateVariable("b", "false", "bool"));
sv4.add(new StateVariable("c", "true", "bool"));
State s4 = new State(sv4, 7.0);
ArrayList<StateVariable> sv5 = new ArrayList<>();
sv5.add(new StateVariable("a", "false", "bool"));
sv5.add(new StateVariable("b", "false", "bool"));
sv5.add(new StateVariable("c", "true", "bool"));
State s5 = new State(sv5, 8.0);
ArrayList<State> states = new ArrayList<>();
states.add(s0);
states.add(s1);
states.add(s2);
states.add(s3);
states.add(s4);
states.add(s5);
Trace t = new Trace(states);
//System.out.print(t.toString());
MtlExprParser parser = new MtlExprParser();
MtlFormula phi = parser.parse("(a || b) U[0,30] c");
//System.out.println("Formula () : "+ phi);
MtlMonitor monitor = new MtlMonitor(null);
int m_verdict = monitor.check(phi, t);
String s_verdict = "";
if(m_verdict == 0) s_verdict = "False";
else if(m_verdict == 1) s_verdict = "True";
else if(m_verdict == 2) s_verdict = "Not able to conclude";
System.out.println("Verdict : " + s_verdict);
}
public static void test17() {
ArrayList<StateVariable> sv0 = new ArrayList<>();
......@@ -91,6 +158,7 @@ public class TestFormulaModel {
}
}
public static void test16(){
......@@ -520,7 +588,7 @@ public class TestFormulaModel {
MtlExprParser parser = new MtlExprParser();
Filter f = new Filter();
MtlFormula phi = parser.parse(" N(abs (Master.val-Slave.val)< (5-3) || !sync)");
MtlFormula phi = parser.parse("(F[1,3](a)||exp(x+5)<3)R (b && c)");
MtlFormula filtered_phi = f.replaceEventually(f.replaceGlobally(phi));
// ArrayList<String> vars = filtered_phi.getDataVariablesList();
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment