New to Alloy - discussions and questions

Alloy 6
1

Hi everyone!

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.

Since 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.

2

Your approach looks interesting: care to share a minimal working example?

Regarding state machines, let me link to this post which describes an approach that works well in practice.

Finally, regarding your question, as I said in the thread you referred to, nothing prevents you to add a fact in this style:

fact { always all m: Machine | m = m' implies m.field' = m.field }

Depending on the context, it may be ok.

3

Hi @grayswandyr! Thank for your response

Let me show you a minimal toy working example I’ve done:

let unchanged[r] { (r)' = (r) } 

one sig System {
  var wind: one Int,
  var temp: one Int
} {
  wind >= 0
  wind =< 10
  temp >= 10
  temp =< 25
}

pred initial_state {
  System.wind = 0
  System.temp = 10
}

-- EARMARKING

enum ACTIONS { ACTION_1, ACTION_2, ACTION_3 }

one sig EARMARKING {
  var taken_actions: set ACTIONS
}

-- ENABLING CONDITIONS

pred enabling_condition_1 {
  System.wind < 10
}

pred enabling_condition_2 {
  System.temp < 25
}

pred enabling_condition_3 {
  System.wind = 10
  System.temp = 25
}

-- ACTIONS

pred action_1 {
  System.wind' = System.wind.add[2]
}

pred action_2 {
  System.temp' = System.temp.add[5]
}

pred action_3 {
  System.wind' = 0
  System.temp' = 10
}

-- REQUIREMENTS

pred requirement_1 {
  enabling_condition_1 implies (action_1 and (ACTION_1 in EARMARKING.taken_actions))
  else (ACTION_1 not in EARMARKING.taken_actions)
}

pred requirement_2 {
  enabling_condition_2 implies (action_2 and (ACTION_2 in EARMARKING.taken_actions))
  else (ACTION_2 not in EARMARKING.taken_actions)
}

pred requirement_3 {
  enabling_condition_3 implies (action_3 and (ACTION_3 in EARMARKING.taken_actions))
  else (ACTION_3 not in EARMARKING.taken_actions)
}

-- FRAMING

pred is_var_changed[var_changers: ACTIONS] {
  some (EARMARKING.taken_actions & var_changers)
}

pred framing {
  let wind_var_action_changers = ACTION_1 + ACTION_3,
    temp_var_action_changers = ACTION_2 + ACTION_3 {
      (not is_var_changed[wind_var_action_changers]) implies unchanged[System.wind]
      (not is_var_changed[temp_var_action_changers]) implies unchanged[System.temp]
  }
}

-- POSSIBLE STEPS

pred possible_steps {
  requirement_1
  requirement_2
  requirement_3
}

-- FACTS

fact {
  initial_state
  always possible_steps
  always framing
}

give_me_an_instance: run { } for 6 Int

assert variables_cant_take_unspecified_behavior {
  always System.wind != 1
  always System.temp != 12
}

check variables_cant_take_unspecified_behavior for 6 Int

I have read your modelling in your post! Is like we have think similar ideas, implemented little different.

I call ‘requirements’ what you call ‘events’, ‘enabling conditions’ what you call ‘guards’ and ‘actions’ what you call ‘efects’.

Also, your ‘Event Reification’ are my ‘earmarkings’ somehow, but implemented in a different manner, I like how with your way you can know on which specific elements did they act.
In my case, my effects always acts over the same atoms, so I didn’t need to distinguish over which elements they’ve been taken. Anyway I save this idea for future possible use.

Thank you for the fact’s instance! I had read your idea in the referred thread but I didn’t understand how to implement it.
I would also like to understand why m = m' doesn’t implies m.field' = m.field! I mean, what are we saying (at low level maybe?) when we say m = m'? And why the said implication doesn’t holds.

4

Well, what it means is that I’m writing crap because I’m on vacation, with too much heat, and writing on my cell phone, sorry about that!

My point was that you can use constraints to relate the lifecycle of different relations, which may spare you some explicit frame conditions in some situations. The next version of Alloy will also come with fixed and updated meta features that may help writing such constraints.

5

@ale: Another pattern you might find useful is explained in my book Software Abstractions around page 200. Here’s an excerpt:

CleanShot 2023-08-09 at 23.52.17@2x
CleanShot 2023-08-09 at 23.52.17@2x1104×606 49.7 KB

This uses implications in reverse: if a particular variable changed, then a certain action must have happened. This idea is from a paper by Reiter (cited as [57] in the book).

I wonder if your implications for the enabling conditions are too strong. They seem to have the form

enabling condition for event e true implies event e happened

But what happens if the enabling conditions for two actions overlap? Then both have to happen?

6

Hi @grayswandyr, first of all, how good to know that a new version of Alloy is coming and even more that will have these meta features!

Let me say what I think I have understood so you can correct me.
Lets consider the following code:

sig Machine {
  id: one Int
}

fact framing_1 {
  Machine' = Machine
}

fact framing_2 {
  Machine.id' = Machine.id
}

fact framing_3 {
  always all m: Machine | m = m' implies m.field' = m.field
}

Is it that with framing_1 I am stating that the set of all Machine will have the same elements in the next step
For instance, Machine being singleton Machine = Machine' = {Machine$0})?
Or with 2 elements Machine = {Machine$0, Machine$1) and without framing_1 one of them could be ‘deleted’ (or other added), being Machine' = {Machine$1}?
But, even with framing_1, we could have Machine$0.id != Machine$0.id', right? Because the Machine’s atom is the same between both steps, but what it have changed is the relation id.

Then, with framing_2 what we are saying is that the image of the id relation is the same in both steps, right? So, for instance, this couldn’t happen:

Machine = Machine' = {Machine$0, Machine$1}
Machine$0.id = Machine$0.id' = 2
Machine$1.id = 3
Machine$1.id' = 2

But the following it is possible:

Machine = Machine' = {Machine$0, Machine$1}
Machine$0.id = 2
Machine$0.id' = 3
Machine$1.id = 3
Machine$1.id' = 2

So that’s why we need to add the fact you said, framing_3, to do a ‘good framing’.

Well, thank you for your response again.

I hope you are near the sea or some place with water to cool down that heat!

7

Hi @DanielJackson thanks for your response!

Good idea this of the implication in reverse, is like you are doing earmarking and framing altogether at the same time!
I should read the full example in your book or the paper you say to fully understand it.
Because I have some doubts on how that it exactly works. For example, what happens if the same variable can be changed by two different Events?
I also don’t fully understand how is specified with the fact Traces ‘how’ the variable must change. I mean, how gets specified not only that some variable ‘changes’ but also to which value should change.

About your wonder for the enabling conditions being too strong, yes, that’s true. I am doing it because from the language I am going to transpile to Alloy have that semantics. That is, every time an action is enabled is taken and yes, multiple actions can happen simultaneously. We assume that every set of actions which can be enabled at the same time doesn’t have incompatible actions.

Also, congratulations for your anniversary here at the community :partying_face: !

8

I also don’t fully understand how is specified with the fact Traces ‘how’ the variable must change. I mean, how gets specified not only that some variable ‘changes’ but also to which value should change.

I should have noted: the example is in Alloy 4, so the priming just refers to a time point after the event, and the idiom makes objects for the events so that occupant.t, for example, is the value of the occupant variable at time t.