What are the TLA+ source files in the model folder?
23 views
Skip to first unread message
ns
unread,
Feb 2, 2021, 10:44:24 PM2/2/21
Reply to author
Sign in to reply to author
Forward
Sign in to forward
Delete
You do not have permission to delete messages in this group
Copy link
Report message
Show original message
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to tlaplus
I am trying to re-use a model from an older version of a spec that I am developing (because it had all the properties and invariants, paramater values, etc that I needed already set up). When I looked inside the folder for the model I saw copies of all the TLA+ files pertaining to the spec. Why are these duplicated in the model and is it correct to just copy that old model folder and drop it into the new spec? Toolbox doesn't seem to complain and it even happily brings up the model in the new spec, but I do wonder if somehow it might be trying to use those old files
thanks
ns
unread,
Feb 2, 2021, 10:45:52 PM2/2/21
Reply to author
Sign in to reply to author
Forward
Sign in to forward
Delete
You do not have permission to delete messages in this group
Copy link
Report message
Show original message
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to tlaplus
I should add that my newer spec is in a different folder from the old spec, I do this to keep the different versions cleanly seperated