Attachment 21199 Details for Bug 95344 – The test case

The test case

Formula$1.aj (text/plain), 6.74 KB, created by Eric Bodden

on 2005-05-16 07:34:00 EDT

(hide)

Description:

Filename:

MIME Type:

Creator: Eric Bodden

Created: 2005-05-16 07:34:00 EDT

Size: 6.74 KB

patch

obsolete

>package rwth.i2.ltlrv.formula;
>
>import rwth.i2.ltlrv.data.*;
>import rwth.i2.ltlrv.management.*;
>
>public privileged aspect Formula$1 {
>    private PropositionSet currentProps = new PropositionSet();
>    
>    private static final IFormulaFactory factory = VerificationRuntime.getInstance().getFactory();
>    
>    private final String prop1 = "call(* (test.MyLock).lock(Thread)) && target(y) && args(i)";
>    
>    private final String prop0 = "call(* (test.MyLock).lock(Thread)) && target(x) && args(i)";
>    
>    private final String prop2 = "call(* (test.MyLock).lock(Thread)) && target(x) && args(i)";
>    
>    private final String prop4 = "call(* (test.MyLock).unlock(Thread)) && target(x) && args(i)";
>    
>    private final String prop3 = "call(* (test.MyLock).lock(Thread)) && target(x) && args(j)";
>    
>    private final String prop6 = "call(* (test.MyLock).lock(Thread)) && target(y) && args(i)";
>    
>    private final String prop5 = "call(* (test.MyLock).lock(Thread)) && target(y) && args(j)";
>    
>    private final String prop8 = "call(* (test.MyLock).lock(Thread)) && target(x) && args(j)";
>    
>    private final String prop7 = "call(* (test.MyLock).unlock(Thread)) && target(y) && args(j)";
>    
>    private final String prop9 = "call(* (test.MyLock).lock(Thread)) && target(y) && args(i)";
>    
>    private final IFormula originalFormula = factory.G(factory.Not(factory.Impl(factory.Until(factory.Not(factory.Proposition(prop6, new java.lang.String[] { "i", "y" })), factory.And(factory.And(factory.Proposition(prop2, new java.lang.String[] { "i", "x" }), factory.Not(factory.Proposition(prop9, new java.lang.String[] { "i", "y" }))), factory.Until(factory.Not(factory.Proposition(prop4, new java.lang.String[] { "i", "x" })), factory.Proposition(prop1, new java.lang.String[] { "i", "y" })))), factory.G(factory.Until(factory.Not(factory.And(factory.Proposition(prop8, new java.lang.String[] { "j", "x" }), factory.Not(factory.Proposition(prop0, new java.lang.String[] { "i", "x" })))), factory.And(factory.Proposition(prop5, new java.lang.String[] { "j", "y" }), factory.Until(factory.Not(factory.Proposition(prop7, new java.lang.String[] { "j", "y" })), factory.Proposition(prop3, new java.lang.String[] { "j", "x" }))))))));
>    
>    private IAFAState formula = originalFormula.negationNormalForm();
>    
>    public Formula$1() {
>        VerificationRuntime.getInstance().registerFormula("Formula$1", originalFormula);
>    }
>    
>    before(Thread i, test.MyLock x):
>    !within(Formula$1) &&
>      (call(* (test.MyLock).lock(Thread)) && target(x) && args(i)) {
>        final WeakValuesMap bindings = new WeakValuesHashMap();
>        bindings.put("i", i);
>        bindings.put("x", x);
>        currentProps.add(factory.Proposition(prop0, bindings));
>    }
>    
>    before(Thread i, test.MyLock y):
>    !within(Formula$1) &&
>      (call(* (test.MyLock).lock(Thread)) && target(y) && args(i)) {
>        final WeakValuesMap bindings = new WeakValuesHashMap();
>        bindings.put("i", i);
>        bindings.put("y", y);
>        currentProps.add(factory.Proposition(prop1, bindings));
>    }
>    
>    before(Thread i, test.MyLock x):
>    !within(Formula$1) &&
>      (call(* (test.MyLock).lock(Thread)) && target(x) && args(i)) {
>        final WeakValuesMap bindings = new WeakValuesHashMap();
>        bindings.put("i", i);
>        bindings.put("x", x);
>        currentProps.add(factory.Proposition(prop2, bindings));
>    }
>    
>    before(Thread j, test.MyLock x):
>    !within(Formula$1) &&
>      (call(* (test.MyLock).lock(Thread)) && target(x) && args(j)) {
>        final WeakValuesMap bindings = new WeakValuesHashMap();
>        bindings.put("j", j);
>        bindings.put("x", x);
>        currentProps.add(factory.Proposition(prop3, bindings));
>    }
>    
>    before(Thread i, test.MyLock x):
>    !within(Formula$1) &&
>      (call(* (test.MyLock).unlock(Thread)) && target(x) && args(i)) {
>        final WeakValuesMap bindings = new WeakValuesHashMap();
>        bindings.put("i", i);
>        bindings.put("x", x);
>        currentProps.add(factory.Proposition(prop4, bindings));
>    }
>    
>    before(Thread j, test.MyLock y):
>    !within(Formula$1) &&
>      (call(* (test.MyLock).lock(Thread)) && target(y) && args(j)) {
>        final WeakValuesMap bindings = new WeakValuesHashMap();
>        bindings.put("j", j);
>        bindings.put("y", y);
>        currentProps.add(factory.Proposition(prop5, bindings));
>    }
>    
>    before(Thread i, test.MyLock y):
>    !within(Formula$1) &&
>      (call(* (test.MyLock).lock(Thread)) && target(y) && args(i)) {
>        final WeakValuesMap bindings = new WeakValuesHashMap();
>        bindings.put("i", i);
>        bindings.put("y", y);
>        currentProps.add(factory.Proposition(prop6, bindings));
>    }
>    
>    before(Thread j, test.MyLock y):
>    !within(Formula$1) &&
>      (call(* (test.MyLock).unlock(Thread)) && target(y) && args(j)) {
>        final WeakValuesMap bindings = new WeakValuesHashMap();
>        bindings.put("j", j);
>        bindings.put("y", y);
>        currentProps.add(factory.Proposition(prop7, bindings));
>    }
>    
>    before(Thread j, test.MyLock x):
>    !within(Formula$1) &&
>      (call(* (test.MyLock).lock(Thread)) && target(x) && args(j)) {
>        final WeakValuesMap bindings = new WeakValuesHashMap();
>        bindings.put("j", j);
>        bindings.put("x", x);
>        currentProps.add(factory.Proposition(prop8, bindings));
>    }
>    
>    before(Thread i, test.MyLock y):
>    !within(Formula$1) &&
>      (call(* (test.MyLock).lock(Thread)) && target(y) && args(i)) {
>        final WeakValuesMap bindings = new WeakValuesHashMap();
>        bindings.put("i", i);
>        bindings.put("y", y);
>        currentProps.add(factory.Proposition(prop9, bindings));
>    }
>    
>    before():
>    !within(Formula$1) &&
>      (call(* (test.MyLock).lock(Thread)) && target(test.MyLock) && args(Thread) || call(* (test.MyLock).lock(Thread)) && target(test.MyLock) && args(Thread) || call(* (test.MyLock).lock(Thread)) && target(test.MyLock) && args(Thread) || call(* (test.MyLock).lock(Thread)) && target(test.MyLock) && args(Thread) || call(* (test.MyLock).unlock(Thread)) && target(test.MyLock) && args(Thread) || call(* (test.MyLock).lock(Thread)) && target(test.MyLock) && args(Thread) || call(* (test.MyLock).lock(Thread)) && target(test.MyLock) && args(Thread) || call(* (test.MyLock).unlock(Thread)) && target(test.MyLock) && args(Thread) || call(* (test.MyLock).lock(Thread)) && target(test.MyLock) && args(Thread) || call(* (test.MyLock).lock(Thread)) && target(test.MyLock) && args(Thread)) {
>        formula = formula.alternatingTransition(currentProps);
>        VerificationRuntime.getInstance().updateFormula("Formula$1", formula);
>        currentProps.clear();
>    }
>}

Actions: View

Attachments on bug 95344: 21199 | 22410