Alloy Analyzer: how to define "run" until a condition holds?

Question

I have a model to specify tasks and relations between tasks. Actually I have different kinds of relations, but to make it simpler let's suppose only one kind. The simpler code is the following:

open util/ordering[Time]

sig Time {}

abstract sig State {}
lone sig Enabled extends State {}
lone sig Disabled extends State {}

sig Task {
    state : State one -> Time
}

sig Relation {
    relation : Task one -> Task,
}

fact noLoop {
    no a : Task | a not in a.^(Relation.relation)
}

fact trace {
    init[first[]]
    all t : Time - last[] |
        let t' = t.next[] |
            some a : Task |
                execute[a, t, t']
}

pred init [t : Time] {
    Task.state.t = Enabled
}

pred execute[exec : Task, t, t' : Time] {
    exec.state.t = Enabled

    let
        disabledTasks = 
            exec 
            + {a : Task | let r = Relation | a in exec.(r.relation)}
            + {a : Task | a.state.t = Disabled},
        otherTasks = {a : Task | a not in disabledTasks}
    |
        disabledTasks.state.t' = Disabled
        and 
        otherTasks.state.t' = Enabled
}

Initially, all tasks are in the enabled state. When executed, the task goes to the disabled state as well as all the related tasks.

I know I can find instances of the model running, for example:

run execute for 6

This will show me instances with 6 time steps only. Sometimes, at the end of the 6th time step, there will be enabled tasks. I would like to know if there exists a way of asking the Alloy Analyzer to run the execute predicate until all the tasks are disabled. Actually, what I want to show is that this model can always achieve the state where all the tasks are disabled (even if I need to define a limited scope).

Thanks for all the help.

C. M. Sperberg-McQueen C. M. Sperberg-McQueen · Accepted Answer · 2016-01-27T17:26:01

The only arguments to run are the name of the predicate to be run and a scope.

So no, it cannot be done in the way you describe. The problem, however, is not the syntactic restriction of run to two arguments; the problem is that unlike you, Alloy has no intrinsic notion of time, so "until" is not a useful concept in describing things to Alloy.

On the other hand, if you want to run a simulation until some state of affairs is reached, all you have to do is describe that state of affairs in a named predicate, and run that predicate. So: define a predicate that means "all tasks are disabled"; call it all_done. Then define the predicate

pred interesting {
  execute and all_done
}
run interesting for ...

Good luck.

Alloy Analyzer: how to define "run" until a condition holds?

1 Answers