confusing crash when trying to use tla tool box on mac (most recent version 1.5.1)

[Carter Schonwald]

hey all,

when trying to run the hour clock example i've been hitting some crashes, and i'ld love some guidance to understand whats going on!

many many thanks
-Carter

----------------------------- MODULE firstmodel -----------------------------


=============================================================================
\* Modification History
\* Last modified Wed Sep 30 18:27:18 EDT 2015 by carter
\* Created Wed Sep 30 17:49:30 EDT 2015 by carter
EXTENDS Naturals
VARIABLE hr
HCini == hr \in (1 .. 12)
HCnext == hr' = IF hr # 12 THEN hr + 1 ELSE 1
HC == HCini /\ [][HCnext]_hr
-----------------------------------------------------------------------------
THEOREM HC => []HCini
=============================================================================


i get an error / stack trace like so:

TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.NullPointerExceptionjava.lang.NullPointerException
at tlc2.tool.Spec.getPrimedLocs(Spec.java:1787)
at tlc2.tool.AbstractChecker.reportCoverage(AbstractChecker.java:153)
at tlc2.tool.ModelChecker.printSummary(ModelChecker.java:726)
at tlc2.tool.ModelChecker.modelCheck(ModelChecker.java:184)
at tlc2.TLC.process(TLC.java:746)
at tlc2.TLC.main(TLC.java:188)


when i then look at the console output in the tool box i see
@!@!@STARTMSG 2262:0 @!@!@
TLC2 Version 2.07 of 1 June 2015
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2187:0 @!@!@
Running in Model-Checking mode.
@!@!@ENDMSG 2187 @!@!@
@!@!@STARTMSG 2220:0 @!@!@
Starting SANY...
@!@!@ENDMSG 2220 @!@!@
Parsing file MC.tla
Parsing file firstmodel.tla
Parsing file /Applications/tla toolbox 1.5.1/plugins/org.lamport.tlatools_1.0.0.201506011130/tla2sany/StandardModules/TLC.tla
Parsing file /Applications/tla toolbox 1.5.1/plugins/org.lamport.tlatools_1.0.0.201506011130/tla2sany/StandardModules/Naturals.tla
Parsing file /Applications/tla toolbox 1.5.1/plugins/org.lamport.tlatools_1.0.0.201506011130/tla2sany/StandardModules/Sequences.tla
Semantic processing of module firstmodel
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module TLC
Semantic processing of module MC
@!@!@STARTMSG 2219:0 @!@!@
SANY finished.
@!@!@ENDMSG 2219 @!@!@
@!@!@STARTMSG 2185:0 @!@!@
Starting... (2015-09-30 18:27:32)
@!@!@ENDMSG 2185 @!@!@
@!@!@STARTMSG 2189:0 @!@!@
Computing initial states...
@!@!@ENDMSG 2189 @!@!@
@!@!@STARTMSG 2190:0 @!@!@
Finished computing initial states: 0 distinct states generated.
@!@!@ENDMSG 2190 @!@!@
@!@!@STARTMSG 2193:0 @!@!@
Model checking completed. No error has been found.
Estimates of the probability that TLC did not check all reachable states
because two distinct states had the same fingerprint:
calculated (optimistic): val = 0.0
based on the actual fingerprints: val = 1.1E-19
@!@!@ENDMSG 2193 @!@!@
@!@!@STARTMSG 2201:0 @!@!@
The coverage statistics at 2015-09-30 18:27:32
@!@!@ENDMSG 2201 @!@!@
@!@!@STARTMSG 1000:1 @!@!@
TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.NullPointerExceptionjava.lang.NullPointerException
at tlc2.tool.Spec.getPrimedLocs(Spec.java:1787)
at tlc2.tool.AbstractChecker.reportCoverage(AbstractChecker.java:153)
at tlc2.tool.ModelChecker.printSummary(ModelChecker.java:726)
at tlc2.tool.ModelChecker.modelCheck(ModelChecker.java:184)
at tlc2.TLC.process(TLC.java:746)
at tlc2.TLC.main(TLC.java:188)

@!@!@ENDMSG 1000 @!@!@
@!@!@STARTMSG 2186:0 @!@!@
Finished. (2015-09-30 18:27:32)
@!@!@ENDMSG 2186 @!@!@

[Stephan Merz]

Hello Carter,

a line starting with "===" is interpreted as the end of the module, so the TLA+ parser sees an empty module. That's why the Toolbox positions the cursor between the header line and that bottom line and inserts the "modification history" below it. (You may insert lines "------" if you want to have visual delimiters in your specification.)

I presume that you just tried running TLC by clicking on the green triangle without worrying about why the Toolbox told you that there was no behavior specification?

Indeed, TLC could fail more gracefully than by throwing a NullPointerException ...

If you remove the offending line, I believe that everything will work fine.

Best regards,
Stephan

> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at http://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

[Markus Alexander Kuppe]

On 01.10.2015 08:58, Stephan Merz wrote:
> a line starting with "===" is interpreted as the end of the module, so the TLA+ parser sees an empty module. That's why the Toolbox positions the cursor between the header line and that bottom line and inserts the "modification history" below it. (You may insert lines "------" if you want to have visual delimiters in your specification.)
>
> I presume that you just tried running TLC by clicking on the green triangle without worrying about why the Toolbox told you that there was no behavior specification?
>
> Indeed, TLC could fail more gracefully than by throwing a NullPointerException ...
>
> If you remove the offending line, I believe that everything will work fine.

Hi Carter,

thanks for reporting. The next TLC release won't throw an NPE anymore.

Cheers
Markus

[Carter Schonwald]

I'm not quite certain what I did, but I did finally get it working later that evening. Thanks!

-Carter