
module vending_machine
{
  type state_t = enum { pay, select, soda, beer };
  var state : state_t;

  init {
    state = pay;
  }

  transition {
    // Insert coin
    if state == pay {
      state' = select;
    }
    // Get soda
    else if state == select {
      state' = soda;
    }
    // Get beer
    else if state == select {
      state' = beer;
    }
  }
}

module main
{
  var coin_inserted : boolean;

  instance vm : vending_machine;

  init {
    coin_inserted = false;
  }

  next {
    // Liveness property: Drink can only be delivered after a coin is inserted
    if vm.state == select {
      assert coin_inserted;
    }
  }

  transition {
    // Insert coin action
    if !coin_inserted {
      coin_inserted' = true;
    }
  }
}
