Specifiing a set of model values using INSTANCE

[abdallah kerim]

Hello everyone,

 I am trying to generate a module that is directly model-checkable by TLC. Below is the module I have written. In this module,  I tried to substitute a constant NODE,  declared in the instantiated module(tsp),  by a set of model values.

 ------------------------------- MODULE tspIns -------------------------------

 VARIABLES at, visited

 INSTANCE tsp WITH NODE <- {n1,n2} =============================================

But when I run the parser, I get the following error :

Unknown operator 'n1'

Unknown operator 'n2' 

Is there any way to fix this without using a config file or typing the values manually  in the Model Overview page of the toolbox ide?

 

Kind Greetings,

Kerim

[Stephan Merz]

Model values are introduced in configurations, not in TLA+ specifications. If you just need the values n1, n2 for model checking, substitute {n1,n2} for the parameter Node in module tsp and check "Set of model values" when using the Toolbox.

If, however, you want to refer to n1 and n2 in module tspins for another reason, declare n1 and n2 as constant parameters and substitute the model values n1 and n2 for those parameters in the Toolbox.

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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/811ebdb3-b9e2-4b77-8b41-1fea5511178cn%40googlegroups.com.

[abdallah kerim]

Thank you Stephan for your response.