I’m new at Alloy and I am using it and I will going to use it to try to achieve a transpiler from a particular existing specification language to Alloy and use the capabilities of Alloy on the models written in the source language.
I have just read the following reply: Alloy 6 vs. TLA+ - #21 by alexshirley and since I am facing with lots of the
nice features and
pain points which @alexshirley describes I wanted to introduce myself and tell how I am working around the difficulties. So maybe they are of help to someone, and also maybe someone came to a better solution and wants to share it. I also want to ask for some clarification on a particular matter, which has been pointed out in @alexshirley post too.
Since I think this is will come quite large and kind of diverts the topic where that reply has been done, I decided to open a new topic.
First I will talk about variables being able to change when their behavior isn’t explicitly stated.
actions word has been already used, I will keep using that term for the predicates/functions we write in Alloy that specifies how our system must change, that is, which actions can be taken over it step by step.
I will also call
system variables to the variables over which our system has control and that shouldn’t change except they are explicitly changed (by an action).
To solve this problem I took this path:
I am using ‘earmarkers’ to know which action is being taken at each step. That is, I define an
enum (lets call it ACTIONS) with all the actions, then I define an signature with a field which is a set of ACTIONS. Then every time an action is taken I add the correct atom of ACTIONS to the set, and explicitly say that isn’t in the set when the action isn’t taken.
Now, since at the time of writing the specification I know which system variables are modified by each action, that is, I have a map
actions -> systems variables. So I add a fact that for each variable which explicitly keeps it unchanged when no one of the actions which modify it hasn’t been activated.
The second subject is a question I have and I want to clarify. As, also stated by @alexshirley, explicitly specifying that a signature (lets say Machine) remains unchanged (by Machine’ = Machine) doesn’t have the effect of remaining its fields unchanged. For example Machine.number’ could be not the same that Machine.number
Thanks in advance for the help and clarifications you could give me on these matters.