Model is stuck in 'modelchecking' state.

[beala]

If I run this spec:

------------------------------ MODULE scratch ------------------------------
EXTENDS Integers, TLC, Sequences, FiniteSets

Range(t) == {t[i] : i \in DOMAIN t}

CharCount(str) == 
    [c \in Range(str) |-> Cardinality({n \in DOMAIN str : str[n] = c})]

=============================================================================

With "No Behavior Spec" selected in the model, and this added to "Evaluate constant expression"

CharCount(<<'a','a'>>)

And then I run the model, it gets stuck in a "modelchecking" state. I can't stop or restart the model checker. I have to restart the entire toolbox to reset the model's state.

I see this log output on the command line:

Writing files to: Model_1/
Errors in model file found /home/alex/workspace/tla/scratch.toolbox/Model_1/MC.tla

Here are the contents of MC.tla.

---- MODULE MC ----
EXTENDS scratch, TLC

\* Constant expression definition @modelExpressionEval
const_expr_15186293876154000 == 
CharCount(<<'a','a'>>)
----

\* Constant expression ASSUME statement @modelExpressionEval
ASSUME PrintT(<<"$!@$!@$!@$!@$!",const_expr_15186293876154000>>)
----

=============================================================================
\* Modification History
\* Created Wed Feb 14 10:29:47 MST 2018 by alex

Here is my version info:

TLA+ Toolbox provides a user interface for TLA+ Tools. 

This is Version 1.5.6 of 29 January 2018 and includes:
  - SANY Version 2.1 of 23 July 2017
  - TLC Version 2.12 of 29 January 2018
  - PlusCal Version 1.8 of 07 December 2015
  - TLATeX Version 1.0 of 20 September 2017

So it seems that the model checker starts, encounters an error, and quits without reseting the model's state or displaying that error to the user.

[beala]

I guess what's killing the model checker is that single quoted characters aren't valid syntax: CharCount(<<'a','a'>>).

[lemmy]

Related to #103

[lemmy]

Isn't programming great, fixed this one by replacing printf(...) with println(String.format(...)).