K-user mailing list

[Daniele Filaretti <daniele.filaretti AT gmail.com>]

Hi all, 
I'm trying to use the model checking feature no my K definition, which 
currently uses an external parser. I had a look at the CINK example from the 
k distribution, and I'm trying to do something similar. 
In short, it turns out that when the formula I check is true, i got "true" as 
output, but when it is false, I get a Java exception. This is an example:

krun --parser="java -jar Parser-imp.jar" imp-examples/max3.imp --ltlmc "<>Ltl 
eqTo(a, 3)"

> Exception in thread "main" java.lang.IllegalArgumentException: Pair cannot 
> contain null values
>       at edu.uci.ics.jung.graph.util.Pair.<init>(Pair.java:42)
>       at edu.uci.ics.jung.graph.AbstractGraph.addEdge(AbstractGraph.java:60)
>       at edu.uci.ics.jung.graph.AbstractGraph.addEdge(AbstractGraph.java:55)
>       at 
> org.kframework.krun.api.MaudeKRun.parseModelCheckResult(MaudeKRun.java:622)
>       at org.kframework.krun.api.MaudeKRun.modelCheck(MaudeKRun.java:566)
>       at org.kframework.krun.Main.normalExecution(Main.java:331)
>       at org.kframework.krun.Main.execute_Krun(Main.java:1047)
>       at org.kframework.main.Main.main(Main.java:29)

The problem (and the error message) is the same no matter which formula I 
give (e.g. also "False" triggers the same exception). 
I thought this might be due to some error in my semantics, but I tried on IMP 
(using external parser, it's the example from the sdf-2-kast tool) and got 
the same problem. 

I read on the K manual about the (external) parsing issues, and the 
environment variables that krun sets (KRUN_SORT, etc.). Can it be related to 
that? 
Also, I thought that maybe the LTL formulae were not being parsed correctly, 
but since I get true when they are true I don't think it's the case (so, are 
they being parsed by krun right?).

One last detail: in the CINK example, there is a 

> syntax Pgm ::= Stmts | LTLFormula

line, while in my examples I put 

> syntax K::= LTLFormula

instead.

Any idea? 

Thanks a lot as usual! :)

Daniele