python
module main
{
    const max : int; // maximum capacity of both bottle repositories

    var nsoda : int; // number of soda bottles
    var nbeer : int; // number of beer bottles

    var sget : bool; // action to get a soda bottle
    var bget : bool; // action to get a beer bottle
    var refill : bool; // action to refill both repositories
    var coin : bool; // action to insert a coin

    location start;
    location select;

    transition start_coin : start -> select
    {
        guard true;
        action coin;
    }

    transition start_refill : start -> start
    {
        guard true;
        action refill;
        nsoda := max;
        nbeer := max;
    }

    transition select_sget : select -> start
    {
        guard nsoda > 0;
        action sget;
        nsoda := nsoda - 1;
    }

    transition select_bget : select -> start
    {
        guard nbeer > 0;
        action bget;
        nbeer := nbeer - 1;
    }

    transition select_ret_coin : select -> start
    {
        guard nsoda == 0 && nbeer == 0;
        action ret_coin;
    }

    init start {
        nsoda := max;
        nbeer := max;
    }

    invariant non_negative_bottles : nsoda >= 0 && nbeer >= 0;
}
