////////////////////////////////////////////////////////////////////
//
// RDDL MDP version without enums of the Dice Game demo domain for 
// IPC 2018 by Thomas Keller (tho.keller [at] unibas.ch).
//
// This is a simple domain to show the usage of enum-valued
// state-fluents. In each step, one die may be rolled, and the reward is
// the sum of the pins on all (not just the rolled) die.
//
////////////////////////////////////////////////////////////////////

domain dice_game_demo_mdp {
    requirements = { 
        reward-deterministic,
        preconditions
    };

    types {
        die : object;
    };

    pvariables {
        // state-fluents to represent the value of each die
        die-value-is-one(die)        : {state-fluent, bool, default = true};
        die-value-is-two(die)        : {state-fluent, bool, default = false};
        die-value-is-three(die)      : {state-fluent, bool, default = false};
        die-value-is-four(die)       : {state-fluent, bool, default = false};
        die-value-is-five(die)       : {state-fluent, bool, default = false};
        die-value-is-six(die)        : {state-fluent, bool, default = false};

        // interm-fluents to determine if a die-value changes
        die-value-becomes-one(die)   : {interm-fluent, bool, level = 1};
        die-value-becomes-two(die)   : {interm-fluent, bool, level = 2};
        die-value-becomes-three(die) : {interm-fluent, bool, level = 3};
        die-value-becomes-four(die)  : {interm-fluent, bool, level = 4};
        die-value-becomes-five(die)  : {interm-fluent, bool, level = 5};
        die-value-becomes-six(die)   : {interm-fluent, bool, level = 6};

        // action-fluents
        roll(die)       : {action-fluent, bool, default = false};
    };

    cpfs {
        die-value-is-one'(?d) =
            if (roll(?d)) then die-value-becomes-one(?d)
            else die-value-is-one(?d);

        die-value-is-two'(?d) =
            if (roll(?d)) then die-value-becomes-two(?d)
            else die-value-is-two(?d);

        die-value-is-three'(?d) =
            if (roll(?d)) then die-value-becomes-three(?d)
            else die-value-is-three(?d);

        die-value-is-four'(?d) =
            if (roll(?d)) then die-value-becomes-four(?d)
            else die-value-is-four(?d);

        die-value-is-five'(?d) =
            if (roll(?d)) then die-value-becomes-five(?d)
            else die-value-is-five(?d);

        die-value-is-six'(?d) =
            if (roll(?d)) then die-value-becomes-six(?d)
            else die-value-is-six(?d);        

        // Since exactly one of these has to become true, we have to
        // deal with them sequentially (by using interm-fluents of
        // increasing levels) and base each result on the results before        
        die-value-becomes-one(?d) = 
            Bernoulli(1/6);

        die-value-becomes-two(?d) =
            ~die-value-becomes-one(?d) & Bernoulli(1/5);
    
        die-value-becomes-three(?d) =
            ~die-value-becomes-one(?d) & ~die-value-becomes-two(?d) & Bernoulli(1/4);

        die-value-becomes-four(?d) =
            ~die-value-becomes-one(?d) & ~die-value-becomes-two(?d) & ~die-value-becomes-three(?d) & Bernoulli(1/3);

        die-value-becomes-five(?d) =
            ~die-value-becomes-one(?d) & ~die-value-becomes-two(?d) & ~die-value-becomes-three(?d) & ~die-value-becomes-four(?d) & Bernoulli(1/2);

        die-value-becomes-six(?d) =
            ~die-value-becomes-one(?d) & ~die-value-becomes-two(?d) & ~die-value-becomes-three(?d) & ~die-value-becomes-four(?d) & ~die-value-becomes-five(?d);
    };
    
    reward = sum_{?d : die} [ (1 * die-value-is-one(?d))   + (2 * die-value-is-two(?d)) +
                              (3 * die-value-is-three(?d)) + (4 * die-value-is-four(?d)) +
                              (5 * die-value-is-five(?d))  + (6 * die-value-is-six(?d)) ]; 
        
    action-preconditions {
        // only one die may be rolled at a time
        ( sum_{?d : die} [ roll(?d) ] ) <= 1;
    };
}