Traffic signals with Alloy 6's temporal logic

signal.als

module signal

enum LightState { On, Off, Blink }

abstract sig Light {
  var state: one LightState
}

one sig Red, Green extends Light {}

pred stopToGo {
  Red.state   = On
  Green.state = Off

  Red.state'   = Off
  Green.state' = On
}

pred goToCaution {
  Red.state   = Off
  Green.state = On

  Red.state'   = Off
  Green.state' = Blink
}

pred cautionToStop {
  Red.state   = Off
  Green.state = Blink

  Red.state'   = On
  Green.state' = Off
}

pred step {
  stopToGo || goToCaution || cautionToStop
}

pred spec {
  Red.state = On
  Green.state = Off
  always step
}

cannotOnInTheSameTime: check {
  spec => {
    always !(Red.state = On && Green.state = On)
  }
}

canGoInfinitelyManyTimes: check {
  spec => {
    always eventually {
      Red.state   = Off
      Green.state = On
    }
  }
}

run { spec }