PROBPLUGIN - LTL Counter-Example View - cannot display a counter example
Description
Environment
Attachments
Gliffy Diagrams
Activity
Jenkins Build Server January 14, 2014 at 1:40 PM
SUCCESS: Integrated in
ProB_eclipse_develop #1282
PROBPLUGIN-90: Bugfix, missing increment when initialisating the names of the atomic propositions in an LTL formula. (plagge: rev 243b8d54c3ff2f9bf6860c081000dbb8db399db0)
de.prob.core/src/de/prob/core/domainobjects/ltl/CounterExample.java
Daniel Plagge January 14, 2014 at 1:26 PM
The fix should be included in the next build.
The problem was a missing increment to an index variable (i++) when initialising the names of the atomic formulas. Thus only formulas with max. one atomic sub-formula worked correctly.
It seems that the error was introduced by me during a refactoring.
Daniel Plagge January 14, 2014 at 10:03 AM
Yes, I can reproduce the problem and look into it.
Michael Leuschel January 14, 2014 at 8:50 AM
Try with the formula
G({neq0:L(cur)} => X {neq2:L(cur) or neq0:L(cur)})
There should be a counter example but it is not displayed.
Daniel Plagge January 14, 2014 at 4:57 AM
Hallo,
I cannot reproduce the problem. No counter-example is found. There shouldn't be a counter-example, or should it?
The left hand side of the implication is true only in s2, the next state of s2 is s1 or s3.
L(s1)={neq0} and L(s3)={neq2}, the right hand side it thus true, too.
Bests
Daniel
Details
Details
Assignee
Michael LeuschelReporter
Michael LeuschelPriority
Major
Hallo,
Benutze gerade LTL für die Vorlesung.
Bei einer Formel wird das Gegenbeispiel nicht angezeigt. Hast Du eine Ahnung was da los ist?
G ( {neq1:L(cur)} => X {neq2:L(cur) or neq0:L(cur)})
Gruss,
Michael
context Kripke
sets S AP
constants R L s1 s2 s3 neq0 neq1 neq2 S0
axioms
@axm1 partition(S, {s1}, {s2}, {s3})
@axm2 partition(AP, {neq0}, {neq1}, {neq2})
@axm3 R∈ S↔S ∧ dom(R)=S
@axm4 L∈ S→ℙ(AP)
@axm5 S0 ⊆ S
@prob_axm1 S0 = {s1}
@prob_axm2 R = {s1↦s2, s2↦s1, s2↦s3, s3↦s2}
@prob_axm3 L = {s1↦{neq0}, s2↦{neq1}, s3↦{neq2}}
end
machine Kripke_Machine sees Kripke
variables cur
invariants @inv1 cur∈S
events
event INITIALISATION begin
@ini cur :∈ S0
end
event step any nxt where @grd cur↦nxt ∈ R then
@a cur ≔ nxt
end
end