State Machines in Dafny

[rsingha108]

Hi, I am trying to write a state machine in dafny in the following way. There are two transition steps and they modify some particular state variables.

datatype State = State(
    u : int,
    v : int,
    w : int,
    x : int,
    y : int,
    z : int,
    sq : seq<int>,
    st : set<int>
)

predicate TransitU(s : State , s' : State)
{
    // Only u changes 
    s'.u == s.u + 1
    // rest stays the same
    && s'.v == s.v
    && s'.w == s.w
    && s'.x == s.x
    && s'.y == s.y
    && s'.z == s.z
    && s'.sq == s.sq
    && s'.st == s.st
}

predicate TransitV(s : State , s' : State)
{
    // Only v changes
    s'.v == s.v + 1
    // rest stays the same
    && s'.v == s.v
    && s'.w == s.w
    && s'.x == s.x
    && s'.y == s.y
    && s'.z == s.z
    && s'.sq == s.sq
    && s'.st == s.st
}

datatype Step = 
    | TransitUStep
    | TransitVStep

predicate NextStep(s: State, s': State, step: Step) {
    match step {
        case TransitUStep => TransitU(s, s')
        case TransitVStep => TransitV(s, s')
    }
}

predicate Next(s: State, s': State) {
    exists step :: NextStep(s, s', step)
}

Is there any smart way in which I can write the variables which stays same in each of these transition steps instead of manually writing them all? i.e. In the transition predicates can I only mention the state variables that are changing?

[racko]

Did you take a look at Modeling Concurrency in Dafny? You may not care about the "concurrency" part, but your example looks a lot like TLA+ and I consider this paper to be a quite general approach to translating TLA+ to Dafny, whether concurrent or not.

[ekaprits]

Yes, Dafny allows for "update expressions", where you can state which part of a datatype/collection changes and the rest remains the same. For example, in your case you could write TransitV as

predicate TransitU(s : State , s' : State)
{
    s' == s.(u := s.u+1)
}

This effectively says: "s' is equal to s, except for field u, which will be equal to s.u+1".

A few more things:

• For collections (e.g. sequence, map), the corresponding syntax is
  s' := s[i := new_value]
• Sometimes parts of your state may never change. One way to not have to deal with these parts not changing is to write your transitions as
  predicate Next(c: Constants, v: Variables, v': Variables) {...}
  and write your overall state as
  datatype State = State(c: Constants, v: Variables)
• This looks like a copy-paste problem, but TransitV is currently vacuous (i.e. can never be taken, equal to false), since it includes
  s'.v == s.v + 1 && s'.v == s.v
• If you want to read more on how to use Dafny to write state machines, you may want to take a look at this class, designed by Jon Howell and me. For example, it includes a more advanced technique on how to structure your state machines to improve their provability.

[rsingha108]

Thanks a lot. This is super helpful.