//////////////////////////////////////////////////////////////////// // // RDDL MDP version of the Recon demo domain for IPC 2018 by Thomas // Keller (tho.keller [at] unibas.ch), based on the IPC 2011 Recon // domain of Tom Walsh. // //////////////////////////////////////////////////////////////////// domain recon_demo_mdp { requirements = { reward-deterministic, preconditions }; types { location : object; tool : object; rover : object; camera : tool; life-detector : tool; }; pvariables { // non-fluents CONNECTED(location, location) : {non-fluent, bool, default = false}; BASE(location) : {non-fluent, bool, default = false}; TOOL-ON(tool, rover) : {non-fluent, bool, default = false}; LIFE-DETECTION-PROB(location) : {non-fluent, real, default = 0.0}; LIFE-DETECTION-PROB-DAMAGED(location) : {non-fluent, real, default = 0.0}; IMPORTANCE(location) : {non-fluent, real, default = 0.0}; DAMAGE-PROB(location) : {non-fluent, real, default = 0.0}; // state-fluents rover-at(rover, location) : {state-fluent, bool, default = false}; damaged(tool) : {state-fluent, bool, default = false}; life-checked(location) : {state-fluent, bool, default = false}; life-detected(location) : {state-fluent, bool, default = false}; picture-taken(location) : {state-fluent, bool, default = false}; // action-fluents move(rover, location) : {action-fluent, bool, default = false}; use-tool(rover, tool) : {action-fluent, bool, default = false}; repair(rover, tool) : {action-fluent, bool, default = false}; }; cpfs { rover-at'(?r, ?loc) = // rover ?r is at location ?loc if it moves there if ( move(?r, ?loc) ) then true // or if it doesn't move somewhere else and is already there else ( ~(exists_{?loc2 : location} move(?r, ?loc2) ) & rover-at(?r, ?loc) ); damaged'(?t) = // if ?t is already damaged, it stays damaged unless it's repaired if ( damaged(?t) ) then ~(exists_{?r: rover} [ repair(?r, ?t) ]) // otherwise, if the rover moves, it is damaged with a probability that depends on the target location // (there is always just a single non-zero element in the sum) else Bernoulli( sum_{?loc : location, ?r: rover} [ move(?r, ?loc) * TOOL-ON(?t, ?r) * DAMAGE-PROB(?loc) ] ); life-checked'(?loc) = // becomes true when a life detector is used and remains true from there on life-checked(?loc) | ( exists_{?r : rover, ?l : life-detector} [ rover-at(?r, ?loc) & use-tool(?r, ?l) ] ); life-detected'(?loc) = // if the life detector is used, life is detected with a probability that is higher if the life detector isn't damaged if ( exists_{?r : rover, ?l : life-detector} [ rover-at(?r, ?loc) & use-tool(?r, ?l) & damaged(?l) ] ) then Bernoulli( LIFE-DETECTION-PROB-DAMAGED(?loc) ) else if ( exists_{?r : rover, ?l : life-detector} [ rover-at(?r, ?loc) & use-tool(?r, ?l) & ~damaged(?l) ] ) then Bernoulli( LIFE-DETECTION-PROB(?loc) ) // otherwise, it doesn't change else life-detected(?loc); picture-taken'(?loc) = // a picture of (life at) a location has been taken if the corresponding action has been executed picture-taken(?loc) | ( exists_{?r : rover, ?c : camera} [ rover-at(?r, ?loc) & use-tool(?r, ?c) ] ); }; reward = // taking a picture of life incurs a reward according to the importance of the location ( sum_{?loc : location} [ ( exists_{?r : rover, ?c : camera} [ rover-at(?r, ?loc) & use-tool(?r, ?c) ] ) * IMPORTANCE(?loc) ] ) // and each move, life-detector usage and repair action of each rover incurs a cost of 1 - ( sum_{?r : rover, ?loc : location} [ move(?r, ?loc) ] ) - ( sum_{?r : rover, ?l : life-detector} [ use-tool(?r, ?l) ] ) - ( sum_{?r : rover, ?t : tool} [ repair(?r, ?t) ] ); action-preconditions { // each rover can execute at most one action per step forall_{?r : rover} [ ( sum_{?loc : location} [ move(?r, ?loc) ] ) + ( sum_{?t : tool} [ use-tool(?r, ?t) + repair(?r, ?t) ] ) <= 1 ]; // rovers can only move to locations that are adjacent to their current location forall_{?r : rover, ?loc1 : location} [ move(?r, ?loc1) => ( exists_{?loc2 : location} [ rover-at(?r, ?loc2) & CONNECTED(?loc1, ?loc2) ] ) ]; // rovers can only repair and use their own tools forall_{?r : rover, ?t : tool} [ repair(?r, ?t) => TOOL-ON(?t, ?r) ]; forall_{?r : rover, ?t : tool} [ use-tool(?r, ?t) => TOOL-ON(?t, ?r) ]; // rovers can use the camera only if it isn't damaged forall_{?r : rover, ?c : camera} [ use-tool(?r, ?c) => ~damaged(?c) ]; // rovers can use the camera only if life was found forall_{?r : rover, ?c : camera} [ use-tool(?r, ?c) => ( exists_{?loc : location} [ rover-at(?r, ?loc) & life-detected(?loc) ] ) ]; // rovers can use the camera only once for each life forall_{?r : rover, ?c : camera} [ use-tool(?r, ?c) => ( forall_{?loc : location} [ ~rover-at(?r, ?loc) | ~picture-taken(?loc) ] ) ]; // rovers can use the life detector only if it hasn't been used in this location before forall_{?r : rover, ?l : life-detector} [ use-tool(?r, ?l) => ~(exists_{?loc : location} [ rover-at(?r, ?loc) & life-checked(?loc) ] ) ]; // rovers can only repair a tool if they are in a base forall_{?r : rover, ?t : tool} [ repair(?r, ?t) => ( exists_{?loc : location} [ BASE(?loc) & rover-at(?r, ?loc) ] ) ]; }; state-invariants { // each rover is at exactly one location forall_{?r : rover} [ (sum_{?loc : location} [ rover-at(?r, ?loc) ]) == 1]; }; }