michelelombardi/jpf-ltl failing own test

[Eddie Loeffen]

I am trying to get jpf-ltl working (the michelelombardi version found at https://bitbucket.org/michelelombardi/jpf-ltl).

I have managed to get it to build, but when I run the test provided I get the output described at the end of this post.

So it seems that JPF runs correctly but then something fails to take in to account the ltl being verified and it thinks everything is OK when it should have failed.

Any ideas? I am using the latest revision of jpf-core (r1202) and the latest jpf-ltl ((r13). I have tried manyother jpf-core revisions to no avail. 

TEST OUTPUT:

########################################

......................................... testing test1()

** this is test_1()

  running jpf with args: +listener=gov.nasa.jpf.ltl.ddfs.InfiniteListener +search.class=gov.nasa.jpf

.ltl.ddfs.DDFSearch +finite=false +vm.storage.class=gov.nasa.jpf.vm.FullStateSet +cg.enumerate_rando

m=true +debug=false

JavaPathfinder v7.0 (rev 1202+) - (C) RIACS/NASA Ames Research Center

====================================================== system under test

gov.nasa.jpf.test.jpfltl.AlwaysDoubleEventuallyTest.runTestMethod()

====================================================== search started: 19/10/14 6:12 PM

FRANCO: in choiceGeneratorSet

FRANCO: in choiceGeneratorSet the id of the cg is: ROOT

FRANCO: in choiceGeneratorSet N. of enabled edges = 3

** this is test_1()

FRANCO: in choiceGeneratorSet

FRANCO: in choiceGeneratorSet the id of the cg is: verifyGetInt(II)

FRANCO: in choiceGeneratorSet N. of enabled edges = 3

FRANCO: in choiceGeneratorSet

FRANCO: in choiceGeneratorSet the id of cg is EdgeCG

FRANCO: in choiceGeneratorSet

FRANCO: in choiceGeneratorSet the id of the cg is: verifyGetInt(II)

FRANCO: in choiceGeneratorSet N. of enabled edges = 3

FRANCO: in choiceGeneratorSet

FRANCO: in choiceGeneratorSet the id of cg is EdgeCG

====================================================== results

no errors detected

====================================================== search finished: 19/10/14 6:12 PM

java.lang.AssertionError: JPF failed to detect error: gov.nasa.jpf.ltl.ddfs.LTLProperty

at gov.nasa.jpf.util.test.TestJPF.fail(TestJPF.java:167)

at gov.nasa.jpf.util.test.TestJPF.propertyViolation(TestJPF.java:991)

at gov.nasa.jpf.util.test.TestJPF.verifyPropertyViolation(TestJPF.java:1006)

at gov.nasa.jpf.test.jpfltl.AlwaysDoubleEventuallyTest.test1(AlwaysDoubleEventuallyTest.java:39)

[Franco Raimondi]

Dear Eddie,
I have not been working on this for a while (in spite of my debug messages in the output below :-).
I hope Michele has a bit of time to look into this (I've cc'ed him, in case he is not following the mailing list).

Thanks,
Franco

> --
>
> ---
> You received this message because you are subscribed to the Google Groups "Java™ Pathfinder" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to java-pathfind...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.