How do I create .cfg files?

JordyMoos commented 6 years ago

I noticed that some examples have .cfg files. Does anyone knows how to create them? I did find a .cfg file somewhere in the in the Model_* directories but those config files seem to have added numbers to variable names.

Can I generate a clean .cfg file somehow?

Example: https://github.com/tlaplus/Examples/tree/master/specifications/Prisoners https://github.com/tlaplus/Examples/blob/master/specifications/Prisoners/Prisoners.cfg

lemmy commented 6 years ago

@JordyMoos The TLA Toolbox creates the .cfg files from its visual model representation for you. You don't have to manually edit .cfg files at all.

muenchnerkindl commented 6 years ago

Hello Jordy,

as Markus already said, the Toolbox creates the .cfg files for you. In the old days, users had to write .cfg files themselves (and this is still true if you use TLC from the command line): a TLA+ specification usually describes an infinite-state system (or a family of systems), and the configuration describes a finite-state instance of the system. Config files are described in "Specifying Systems", but for all practical purposes, you don't have to worry about them today.

Regards, Stephan

From: "Jordy Moos" notifications@github.com To: "tlaplus/Examples" Examples@noreply.github.com Cc: "Subscribed" subscribed@noreply.github.com Sent: Wednesday, August 22, 2018 12:15:09 PM Subject: [tlaplus/Examples] How do I create .cfg files? (#6)

I noticed that some examples have .cfg files. Does anyone knows how to create them? I did find a .cfg file somewhere in the in the Model_* directories but those config files seem to have added numbers to variable names.

Can I generate a clean .cfg file somehow?

[ https://github.com/tlaplus/Examples/tree/master/specifications/Prisoners | https://github.com/tlaplus/Examples/tree/master/specifications/Prisoners ]

— You are receiving this because you are subscribed to this thread. Reply to this email directly, [ https://github.com/tlaplus/Examples/issues/6 | view it on GitHub ] , or [ https://github.com/notifications/unsubscribe-auth/AHIrdaK1VkKpwLKKc4hPyr6CLREkGbU5ks5uTS8sgaJpZM4WHX_r | mute the thread ] .

JordyMoos commented 6 years ago

Thanks for the answers and clarifications @lemmy @muenchnerkindl

lemmy commented 6 years ago

Two minor additions: 1) The .cfg files - created by the Toolbox - define the variable values in the MC.tla instead of directly in MC.cfg. This is why you see those funny looking variable names in MC.cfg. 2) You can run command line TLC also on the MC.tla/MC.cfg generated by the Toolbox. Replace your spec's name with "MC", e.g. java -jar tla2tools.jar MC

tlaplus / Examples

How do I create .cfg files? #6