PROBPLUGIN - LTL Counter-Example View - cannot display a counter example

Description

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

Environment

None

Attachments

2

Gliffy Diagrams

Activity

Show:

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

Fixed

Details

Assignee

Reporter

Priority

Created January 13, 2014 at 10:26 AM
Updated January 14, 2014 at 1:40 PM
Resolved January 14, 2014 at 1:26 PM