[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: pluscal, tla+ and tekker algorithm

You didn't say if the translation succeeded.  It probably did, since

you didn't indicate that it produced an error message.  You could find

out by looking at the tla file to make sure that it put the

translation there.


TLC's console output makes it pretty clear if there was an error.

Since you don't know if it it found an error, it probably didn't.  But

we'd have to see the console output to be sure.  But assuming the

translation succeeded and TLC found no error, this means that you have

correctly specified some protocol that has a finite number of

reachable states.  What else it means depends on what the

configuration file told it to check.  You also didn't say what was in

the configuration file.


But before you go any further, you should stop running TLC from a shell

and run it from the Toolbox.  See the TLA+ web page to find out how to

download and install the Toolbox.