toomanybananas.model

/*
 * Copyright (c) 2016, Salesforce.com, Inc.
 * All rights reserved.
 * Licensed under the MIT license.
 * For full license text, see LICENSE.md file in the repo root or
 * https://opensource.org/licenses/MIT
 */

var bananas : 0..100 = 2;
var notePresent: Boolean;
type Person : either {
  Happy,
  Hungry,
  GoingToStore,
  ReturningFromStore {
    carrying: 0..8
  }
};
var roommates: Array<Person>[1..5];

rule step for state in roommates {
  match state {
    Happy {
      state = Hungry;
    }

    Hungry {
      if bananas == 0 {
        if (notePresent) {
          // Roommate at store: try again later
        } else {
          notePresent = True;
          state = GoingToStore;
        }
      } else {
        bananas -= 1;
        state = Happy;
      }
    }

    GoingToStore {
      state = ReturningFromStore {
        carrying: urandomRange(0, 8)
      };
    }

    ReturningFromStore(bag) {
      bananas += bag.carrying;
      notePresent = False;
      state = Hungry;
    }
  }
}

invariant BananaLimit {
  assert bananas <= 8;
}