[tlaplus] Specifiing a set of model values using INSTANCE

[abdallah kerim <alanturing165@xxxxxxxxx>]

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

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