On Tuesday, February 2, 2021 at 7:44:24 PM UTC-8 ns wrote:
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