How to specify "global" frame condition in Alloy6?

I am trying to model temporal process using for reference Formal Software Design with Alloy 6 - Protocol design chapter. I would like to know how to make frame conditions in predicates less verbose.

Toy example:

Let's say that I have concept of Employee who can be logged into Machine and can be present at Machine or in MeasureRoom. Machine can be in one of multiple states: NoLogin, Work and Measuring. Machine has currently active Tool and other Tools, which change activity in different part of model (included in example just to have bigger frame conditions).

enum MachineState { NoLogin, Work, Measuring }

abstract sig Location {}

some sig Tool {}

one sig Machine extends Location {
  var login: lone Employee,
  var state: one MachineState,
  var tools: some Tool,
  var activeTool: lone Tool
}

one sig NotAtWork extends Location {}

one sig MeasureRoom extends Location {}

one sig Employee {
  var location: one Location
}

Then I specify initial state, in which Employee is NotAtWork.

fact init {
  Employee.location = NotAtWork

  no Machine.login
  Machine.state = NoLogin

  Machine.tools = Tool
  no Machine.activeTool
}

Finally transitions between different states (for example, login, measuring_begin and measuring_end):

pred login {
  Machine.state = NoLogin // Guard condition.

  // Effects:
  Machine.state' = Work
  Machine.login' = Employee
  Employee.location' = Machine
}

pred measuring_begin {
  Machine.state = Work // Guard condition.

  // Effects:
  Machine.state' = Measuring
  Employee.location' = MeasureRoom
  
  // Frame conditions - **how to make these less verbose?**:
  Machine.login' = Machine.login
  Machine.tools' = Machine.tools
  Machine.activeTool' = Machine.activeTool
}

pred measuring_end {
  Machine.state = Measuring // Guard condition.

  // Effects:
  Machine.state' = Work
  Employee.location' = Machine

  // Frame conditions - **how to make these less verbose?**:
  Machine.login' = Machine.login
  Machine.tools' = Machine.tools
  Machine.activeTool' = Machine.activeTool
}


fact transition {
    always (
        login or measuring_begin or measuring_end
    )
}

run example {
    eventually measuring_end
}

So more concretely, is it possible to write concise frame condition, that would ensure that new state is identical to previous one except for effects? I understand it may not be possible, since predicates (if I understand correctly), do not mutate state, but just specify search criteria for possible future states.

Solution

You're right that predicates (encoding events) just constrain future states. And because constraints can be arbitrary formulas, it seems impossible to infer frame conditions out of effects. One solution, not currently implemented in Alloy and which would change the language a lot, would be to restrict the syntax of effects in such a way that the said inference would be possible.

Meanwhile, there are a few approaches to simplify your frame conditions. For instance, you can rely on a macro to define an unchanged keyword (macros are a fragile, untyped, parametrized expressions or constraints). E.g.:

let unchanged[r] { ((r) = (r)') } // mind the parentheses

pred measuring_begin {
  ...
  // Frame conditions 
  unchanged[Machine.login]
  unchanged[Machine.tools]
  unchanged[Machine.activeTool]
}

In your case, as there's only one Machine, you may even get rid of the Machine. part and write unchanged[login].

Another approach is to rely on Reiter-style frame conditions (see e.g. these slides by Daniel Jackson (in Alloy 4)). In this approach, you write frame conditions, in a global fact, saying that if relation r changes, it's only because of this or that event. E.g. for login:

fact {
  always {
    (unchanged[Machine.login] or login)
    (unchanged[state] or login or measuring_begin or measuring_end)
    ...
  }
}

Depending on whether events change a lot of state variables or not, one out of local frame conditions vs. global Reiter-style frame conditions will be shorter than the other.

Finally, if you have non-one sigs in your model, you can often express an effect and a frame condition on a field in a single constraint. See the box "Specifying global effects" here.

EDIT: fixed a typo.