localhost:Semaphore Simon$ java -classpath /Applications/toolbox/tla/ tlc2.TLC Sem0_Prog.tla
TLC2 Version 2.07 of 1 June 2015
Running in Model-Checking mode.
Parsing file Sem0_Prog.tla
Parsing file /Applications/toolbox/tla/tla2sany/StandardModules/Integers.tla
Parsing file /Applications/toolbox/tla/tla2sany/StandardModules/Sequences.tla
Parsing file /Applications/toolbox/tla/tla2sany/StandardModules/Naturals.tla
Parsing file Sem0_Spec.tla
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module Sequences
Semantic processing of module Sem0_Spec
Semantic processing of module Sem0_Prog
Starting... (2016-04-16 12:37:39)
Error: 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.RuntimeException: The constant parameter Pcs is not assigned a value by the configuration file.
Finished. (2016-04-16 12:37:39)
Sorry, I hadn't seen that. Thanks!Simon
On Saturday, April 16, 2016 at 10:37:26 AM UTC-4, Stephan Merz wrote:Yes, of course. Please check out the documentation at http://research.microsoft.com/
> On 16 Apr 2016, at 15:53, Simon Hudon <simo...@xxxxxxxxx> wrote:
> I would like to include my TLA+ specifications into my test suite. Is there a way of invoking the model checker from the command line?
> 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 tlaplu...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/
> For more options, visit https://groups.google.com/d/