Commit 0ce7d245 authored by LotfiMed's avatar LotfiMed
Browse files

fixed bug in LTL monitor : adding multiple times the parametric variable

parent db11429d
This diff is collapsed.
......@@ -300,13 +300,18 @@ public class LtlMonitor extends ujf.verimag.sbip.monitor.Monitor implements Runn
formula = (LtlFormula)filter.replaceEventually((LtlFormula)filter.replaceGlobally(formula));
// System.out.println("Checking ... "+formula);
int i = 0;
boolean addedVariable = false;
while(!formula.isTerminal() || gen.getStatesSize() > 1){
State state = gen.getModelState(0);
if(state!=null)
if(state!=null && !addedVariable) {
state.addVariable(parametricVariable);
addedVariable = true;
}
State next_state = gen.getModelState(1);
if(state != null && next_state!=null){
addedVariable = false;
System.out.println(state);
if(!formula.isTerminal()){
LtlFormula f1 = rewrite(formula, state, 1);
......@@ -329,6 +334,7 @@ public class LtlMonitor extends ujf.verimag.sbip.monitor.Monitor implements Runn
if(gen.getStatesSize() == 0){
try {
//System.out.println("\twaiting.");
addedVariable = false;
Thread.sleep(0);
} catch (InterruptedException e) {
e.printStackTrace();
......
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