Forcing InProgress state machines to always resolve

Question

I am trying to model executions of concurrent AWS Lambda functions to look for bugs around timing. In my model, once a Lambda is triggered, it should always end up in either a Complete or Failed state. The problem is, I can't figure out how to tell Alloy to throw out any state sequence where Lambdas are still InProgress in the final state.

Here is what I have. In the actual model, there would be side effects of the state transitions which I would want to make assertions about. Basically "once every lambda is complete or failed, X should be impossible".

abstract sig State {}
sig InProgress, Complete, Failed extends State {}

var sig Lambda {
   var state: one State,
} {
  this in Lambda'
}

pred complete[l:Lambda] {
   l.state' in Complete + Failed
}

pred can_step[l:Lambda] {
  l.state = InProgress 
}

pred wait[l:Lambda] {
 l.state' = l.state
}

pred step_lambdas[] {
  all l: Lambda {
     can_step[l] implies (complete[l] or wait[l]) else wait[l]
  }
  lone l: Lambda | complete[l] // only let one lambda complete at at time
}

pred trigger_lambda[] {
  one l: Lambda' | Lambda' = Lambda + l' and l.state' = InProgress
}

pred do_nothing[] {
  Lambda != none
  Lambda = Lambda'
}

fact {
  Lambda = none
  always trigger_lambda or do_nothing
  always step_lambdas
}

check {
  eventually {
    some Lambda
    no l: Lambda | can_step[l] 
  }
}

Update #1: I tried changing the check statement to the below. I believe it should show me a violation with t0, t1, t2 where at t2 there is a Lambda with state = Error. Instead, it shows me a violation with t0, t1 where at t1 there is a Lambda with state = InProgress. I don't see how this violates the check.

...

check {
  some Lambda
  (all l:Lambda |  not can_step[l]) implies all l:Lambda | l.state = Complete
}

Answer 1

I figured it out. I need to express the check in the form "All lambdas must always be able to step or be in a completed state."

check {
  always all l:Lambda | can_step[l] or l.state in Complete
}

Complete model which finds a counterexample where a lambda ends in Failed state.

abstract sig State {}
sig InProgress, Complete, Failed extends State {}

var sig Lambda {
   var state: one State,
} {
  this in Lambda'
}

pred complete[l:Lambda] {
   l.state' in Complete + Failed
}

pred can_step[l:Lambda] {
  l.state = InProgress
}

pred wait[l:Lambda] {
 l.state' = l.state
}

pred step_lambdas[] {
  all l: Lambda {
     can_step[l] implies (complete[l] or wait[l]) else wait[l]
  }
  lone l: Lambda | complete[l] // only let one lambda complete at at time
}

pred trigger_lambda[] {
  one l: Lambda' | Lambda' = Lambda + l' and l.state' = InProgress
}

pred do_nothing[] {
  Lambda != none
  Lambda = Lambda'
}

fact {
  Lambda = none
  always trigger_lambda or do_nothing
  always step_lambdas
}

check {
  always all l:Lambda | can_step[l] or l.state in Complete
}