Re: [tlaplus] confusing crash when trying to use tla tool box on mac (most recent version 1.5.1)

[Stephan Merz <stepha...@xxxxxxxxx>]

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


> On 01 Oct 2015, at 00:30, Carter Schonwald <carter.s...@xxxxxxxxx> wrote:
> 
> 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 @!@!@
> 
> -- 
> 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...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at http://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.