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

[Carter Schonwald <carter.s...@xxxxxxxxx>]

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 @!@!@