sp
/
Minigrid2PRISM
1
0
Fork 0
Code Issues 5 Pull Requests 1 Projects Releases Wiki Activity
Labels Milestones
New Pull Request

Add Functionality to Change Generated Code #17

Open
tknoll wants to merge 19 commits from overwrites into modeltype
Conversation 4 Commits 19 Files Changed 19
19 changed files with 470 additions and 132 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 37
      CMakeLists.txt
  2. 31
      exampleConfig.yaml
  3. 23
      examples/example_guards.prism
  4. 17
      examples/example_guards.txt
  5. 19
      examples/example_guards.yaml
  6. 17
      examples/example_module.txt
  7. 36
      examples/example_module.yaml
  8. 13
      examples/example_probabilities.txt
  9. 5
      examples/example_probabilities.yaml
  10. 30
      main.cpp
  11. 62
      util/ConfigYaml.cpp
  12. 33
      util/ConfigYaml.h
  13. 27
      util/Grid.cpp
  14. 6
      util/Grid.h
  15. 5
      util/MinigridGrammar.h
  16. 36
      util/PrismFormulaPrinter.cpp
  17. 174
      util/PrismModulesPrinter.cpp
  18. 10
      util/PrismModulesPrinter.h
  19. 7
      util/cell.h

37
CMakeLists.txt
View File

@ -1,26 +1,25 @@
include(util/CMakeLists.txt)
set(CMAKE_CXX_STANDARD 20)
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D__FILENAME__='\"$(subst ${CMAKE_SOURCE_DIR}/,,$(abspath $<))\"'")
add_definitions(-DLOG_DEBUG)
cmake_minimum_required(VERSION 3.0...3.22)
set(CMAKE_BUILD_TYPE Debug)
project(
Minigrid2PRISM
VERSION 0.1
LANGUAGES CXX)
set(CMAKE_CXX_STANDARD 20)
include(util/CMakeLists.txt)
include(FetchContent)
FetchContent_Declare(
yaml-cpp
GIT_REPOSITORY https://github.com/jbeder/yaml-cpp.git
GIT_TAG master
OVERRIDE_FIND_PACKAGE
)
FetchContent_GetProperties(yaml-cpp)
if(NOT yaml-cpp_POPULATED)
message(STATUS "Fetching yaml-cpp...")
FetchContent_Populate(yaml-cpp)
add_subdirectory(${yaml-cpp_SOURCE_DIR} ${yaml-cpp_BINARY_DIR})
endif()
FetchContent_MakeAvailable(yaml-cpp)
add_executable(main ${SRCS} main.cpp)
find_package(yaml-cpp)
add_executable(main
${SRCS}
main.cpp
)
target_link_libraries(main pthread yaml-cpp::yaml-cpp)

31
exampleConfig.yaml
View File

@ -1,7 +1,9 @@
---
labels:
- label: "AgentIsInGoal"
text: "AgentIsInGoal"
# labels:
# - label: "AgentIsInGoal"
# text: "AgentIsInGoal"
# - label: "Hallo"
# text: "AgentIsInGoal"
# constants:
# - constant: "prop_slippery_turn"
@ -9,25 +11,34 @@ labels:
# value: "9/9"
# overwrite: True
probabilities:
- probability: "FaultProbability"
properties:
- property: "FaultProbability"
value: 0.2
- probability: "ProbForwardIntended"
- property: "ProbForwardIntended"
value: 0.1
- probability: "ProbTurnIntended"
- property: "ProbTurnIntended"
value: 0.1
# - property: "modeltype"
# value: "smg"
modules:
- module: "Agent"
# overwrite: True
# module_text: |
# NewModule
# True
commands:
- action: "[Agent_turn_left]"
guard: "AgentIsOnSlippery"
update: "True"
guard: "viewAgent=3"
overwrite: True
index: 1
- action: "[Agent_turn_left]"
update: "(viewAgent'=3)"
overwrite: True
index: 3
- action: "[Agent_turn_right]"
guard: "AgentIsOnSlippery"
update: "True"
update: "(viewAgent'=3)"
overwrite: True
index: [0,1]
...

23
examples/example_guards.prism
View File

@ -0,0 +1,23 @@
mdp
formula AgentCannotMoveEastWall = (colAgent=1&rowAgent=2) | (colAgent=4&rowAgent=2) | (colAgent=4&rowAgent=3) | (colAgent=4&rowAgent=4) | (colAgent=4&rowAgent=1);
formula AgentCannotMoveNorthWall = (colAgent=1&rowAgent=1) | (colAgent=2&rowAgent=1) | (colAgent=3&rowAgent=1) | (colAgent=2&rowAgent=3) | (colAgent=3&rowAgent=3) | (colAgent=4&rowAgent=1);
formula AgentCannotMoveSouthWall = (colAgent=2&rowAgent=1) | (colAgent=3&rowAgent=1) | (colAgent=1&rowAgent=4) | (colAgent=2&rowAgent=4) | (colAgent=3&rowAgent=4) | (colAgent=4&rowAgent=4);
formula AgentCannotMoveWestWall = (colAgent=1&rowAgent=1) | (colAgent=1&rowAgent=2) | (colAgent=4&rowAgent=2) | (colAgent=1&rowAgent=3) | (colAgent=1&rowAgent=4);
formula AgentIsOnSlippery = false;
module Agent
colAgent : [1..4] init 4;
rowAgent : [1..4] init 1;
viewAgent : [0..3] init 1;
[Agent_turn_right] !AgentIsOnOneWay-> 1.000000: (viewAgent'=mod(viewAgent+1,4));
[Agent_turn_left] !AgentIsOnOneWay-> 1.000000: (viewAgent'=viewAgent-1);
[Agent_turn_left] !AgentIsOnOneWay-> 1.000000: (viewAgent'=3);
[Agent_move_North] viewAgent=3 & !AgentCannotMoveNorthWall -> 1.000000: (rowAgent'=rowAgent-1);
[Agent_move_East] colAgent != 1 & rowAgent != 1-> 1.000000: (colAgent'=colAgent+1);
[Agent_move_South] viewAgent=1 & !AgentCannotMoveSouthWall -> 1.000000: (rowAgent'=rowAgent+1);
[Agent_move_West] viewAgent=2 & !AgentCannotMoveWestWall -> 1.000000: (colAgent'=colAgent-1);
endmodule
formula AgentIsOnOneWay = (colAgent=2&rowAgent=1) | (colAgent=3&rowAgent=1); // created through configuration

17
examples/example_guards.txt
View File

@ -0,0 +1,17 @@
WGWGWGWGWGWG
WG XRWG
WG WGWG WG
WG WG
WG WG
WGWGWGWGWGWG
------------
WGWGWGWGWGWG
WG WG
WG WGWG WG
WG WG
WG WG
WGWGWGWGWGWG
------------
------------
ProbTurnIntended:0.85
ProbForwardIntended:0.25

19
examples/example_guards.yaml
View File

@ -0,0 +1,19 @@
---
formulas:
- formula: "AgentIsOnOneWay"
content: "(colAgent=2&rowAgent=1) | (colAgent=3&rowAgent=1)"
modules:
- module: "Agent"
commands:
- action: "[Agent_move_East]"
guard: "colAgent != 1 & rowAgent != 1"
overwrite: True
- action: "[Agent_turn_right]"
guard: "!AgentIsOnOneWay"
overwrite: True
- action: "[Agent_turn_left]"
guard: "!AgentIsOnOneWay"
overwrite: True
index: [0,1]
...

17
examples/example_module.txt
View File

@ -0,0 +1,17 @@
WGWGWGWGWGWGWG
WGZY XRWG
WG WG
WG WG
WG WGWGWGWGWG
WG AYGGWG
WGWGWGWGWGWGWG
--------------
WGWGWGWGWGWGWG
WG WG
WG WG
WG WG
WG WGWGWGWGWG
WG WG
WGWGWGWGWGWGWG
--------------
--------------

36
examples/example_module.yaml
View File

@ -0,0 +1,36 @@
---
properties:
- property: "modeltype"
value: "mdp"
formulas:
- formula: "YellowMovesNorth"
content: "(rowYellow=2 | rowYellow=3 | rowYellow=4) & colYellow=1 & viewYellow=3"
- formula: "YellowMovesSouth"
content: "(rowYellow=2 | rowYellow=3 | rowYellow=4) & colYellow=1 & viewYellow=1"
modules:
- module: "Yellow"
overwrite: True
module_text: |
colYellow : [1..5] init 1;
rowYellow : [1..5] init 1;
viewYellow : [0..3] init 1;
YellowCarryingYellowBall : bool init false;
[Yellow_turn_right] (!YellowMovesSouth & !YellowMovesNorth) -> 1.000000: (viewYellow'=mod(viewYellow+1,4));
[Yellow_turn_left] (!YellowMovesSouth & !YellowMovesNorth) -> 1.000000: (viewYellow'=viewYellow-1);
[Yellow_turn_left] (!YellowMovesSouth & !YellowMovesNorth) -> 1.000000: (viewYellow'=3);
[Yellow_move_North] !YellowMovesSouth & viewYellow=3 & !YellowIsOnGoal & !YellowCannotMoveNorthWall & !YellowCannotMoveConditionally -> 1.000000: (rowYellow'=rowYellow-1);
[Yellow_move_East] !(YellowMovesNorth|YellowMovesSouth) & viewYellow=0 & !YellowIsOnGoal & !YellowCannotMoveEastWall & !YellowCannotMoveConditionally -> 1.000000: (colYellow'=colYellow+1);
[Yellow_move_South] !YellowMovesNorth & viewYellow=1 & !YellowIsOnGoal & !YellowCannotMoveSouthWall & !YellowCannotMoveConditionally -> 1.000000: (rowYellow'=rowYellow+1);
[Yellow_move_West] !(YellowMovesNorth|YellowMovesSouth) & viewYellow=2 & !YellowIsOnGoal & !YellowCannotMoveWestWall & !YellowCannotMoveConditionally -> 1.000000: (colYellow'=colYellow-1);
[Yellow_pickup_YellowBall] !YellowIsCarrying & YellowCannotMoveYellowBall -> (YellowCarryingYellowBall'=true);
[Yellow_drop_YellowBall_north] YellowCarryingYellowBall & viewYellow=3 & !YellowCannotMoveConditionally & !YellowCannotMoveNorthWall -> (YellowCarryingYellowBall'=false);
[Yellow_drop_YellowBall_west] YellowCarryingYellowBall & viewYellow=2 & !YellowCannotMoveConditionally & !YellowCannotMoveWestWall -> (YellowCarryingYellowBall'=false);
[Yellow_drop_YellowBall_south] YellowCarryingYellowBall & viewYellow=1 & !YellowCannotMoveConditionally & !YellowCannotMoveSouthWall -> (YellowCarryingYellowBall'=false);
[Yellow_drop_YellowBall_east] YellowCarryingYellowBall & viewYellow=0 & !YellowCannotMoveConditionally & !YellowCannotMoveEastWall -> (YellowCarryingYellowBall'=false);
...

13
examples/example_probabilities.txt
View File

@ -0,0 +1,13 @@
WGWGWGWG
WGVRXRWG
WGnB WG
WGWGWGWG
--------
WGWGWGWG
WG WG
WGnB WG
WGWGWGWG
--------
--------
ProbTurnIntended:0.85
ProbForwardIntended:0.25

5
examples/example_probabilities.yaml
View File

@ -0,0 +1,5 @@
---
properties:
- property: "ProbForwardIntended"
value: 0.98
...

30
main.cpp
View File

@ -42,7 +42,7 @@ void print_info(boost::spirit::info const& what) {
boost::apply_visitor(walker, what.value);
}
void setProbability(const std::string& gridProperties, const std::vector<Probability> configProperties, const std::string& identifier, float& prop) {
void setProbability(const std::string& gridProperties, const std::vector<Property> configProperties, const std::string& identifier, float& prop) {
auto start_pos = gridProperties.find(identifier);
std::string seperator = ";";
@ -52,7 +52,7 @@ void setProbability(const std::string& gridProperties, const std::vector<Probabi
prop = std::stod(value);
}
auto yaml_config_prop = std::find_if(configProperties.begin(), configProperties.end(), [&identifier](const Probability& obj) -> bool {return obj.probability_ == identifier;} );
auto yaml_config_prop = std::find_if(configProperties.begin(), configProperties.end(), [&identifier](const Property& obj) -> bool {return obj.property == identifier;} );
if (yaml_config_prop != configProperties.end()) {
prop = (*yaml_config_prop).value_;
@ -127,7 +127,7 @@ int main(int argc, char* argv[]) {
cells contentCells;
cells backgroundCells;
std::vector<Configuration> configurations;
std::vector<Probability> probabilities;
std::vector<Property> parsed_properties;
std::map<coordinates, float> stateRewards;
float faultyProbability = 0.0;
float probIntended = 1.0;
@ -142,7 +142,7 @@ int main(int argc, char* argv[]) {
YamlConfigParser parser(configFilename->value(0));
auto parseResult = parser.parseConfiguration();
configurations = parseResult.configurations_;
probabilities = parseResult.probabilities_;
parsed_properties = parseResult.properties_;
}
boost::escaped_list_separator<char> seps('\\', ';', '\n');
@ -158,13 +158,27 @@ int main(int argc, char* argv[]) {
auto probForwardIntendedIdentifier = std::string("ProbForwardIntended");
auto probTurnIntendedIdentifier = std::string("ProbTurnIntended");
setProbability(properties, probabilities, faultProbabilityIdentifier, faultyProbability);
setProbability(properties, probabilities, probForwardIntendedIdentifier, probIntended);
setProbability(properties, probabilities, probTurnIntendedIdentifier, probTurnIntended);
setProbability(properties, parsed_properties, faultProbabilityIdentifier, faultyProbability);
setProbability(properties, parsed_properties, probForwardIntendedIdentifier, probIntended);
setProbability(properties, parsed_properties, probTurnIntendedIdentifier, probTurnIntended);
}
if(ok) {
Grid grid(contentCells, backgroundCells, stateRewards, probIntended, faultyProbability);
auto modelTypeIter = std::find_if(parsed_properties.begin(), parsed_properties.end(), [](const Property& obj) -> bool {return obj.property == "modeltype";});
prism::ModelType modelType = prism::ModelType::MDP;;
if (modelTypeIter != parsed_properties.end()) {
if ((*modelTypeIter).value_str_ == "smg") {
modelType = prism::ModelType::SMG;
} else {
modelType = prism::ModelType::MDP;
}
grid.setModelType(modelType);
}
//grid.printToPrism(std::cout, configurations);
std::stringstream ss;
grid.printToPrism(ss, configurations);
@ -177,7 +191,7 @@ int main(int argc, char* argv[]) {
std::cout << "got: \"" << std::string(e.first, e.last) << '"' << std::endl;
std::cout << "Expectation failure: " << e.what() << " at '" << std::string(e.first,e.last) << "'\n";
} catch(const std::exception& e) {
std::cerr << "Exception '" << typeid(e).name() << "' caught:" << std::endl;
std::cerr << "Exception '" << typeid(e).name() << "' caught:" << e.what() << std::endl;
std::cerr << "\t" << e.what() << std::endl;
std::exit(EXIT_FAILURE);
}

62
util/ConfigYaml.cpp
View File

@ -47,10 +47,10 @@ std::string Formula::createExpression() const {
std::string Command::createExpression() const {
if (overwrite_) {
return action_ + "\t" + guard_ + "-> " + update_ + Configuration::overwrite_identifier_;
return action_ + "\t" + guard_ + " -> " + update_ + Configuration::overwrite_identifier_;
}
return "\t" + action_ + "\t" + guard_ + "-> " + update_+ Configuration::configuration_identifier_;
return "\t" + action_ + "\t" + guard_ + " -> " + update_+ Configuration::configuration_identifier_;
}
std::string Constant::createExpression() const {
@ -74,8 +74,20 @@ bool YAML::convert<Module>::decode(const YAML::Node& node, Module& rhs) {
if (!node.Type() == NodeType::Map) {
return false;
}
rhs.commands_ = node["commands"].as<std::vector<Command>>();
rhs.module_ = node["module"].as<std::string>();
if (node["commands"]) {
rhs.commands_ = node["commands"].as<std::vector<Command>>();
}
if (node["module_text"]) {
rhs.module_text_ = node["module_text"].as<std::string>();
}
if (node["overwrite"]) {
rhs.overwrite_module = node["overwrite"].as<bool>();
}
return true;
}
@ -96,8 +108,13 @@ bool YAML::convert<Command>::decode(const YAML::Node& node, Command& rhs) {
}
rhs.action_ = node["action"].as<std::string>();
if (node["guard"]) {
rhs.guard_ = node["guard"].as<std::string>();
}
if (node["update"]) {
rhs.update_ = node["update"].as<std::string>();
}
if (node["overwrite"]) {
rhs.overwrite_ = node["overwrite"].as<bool>();
@ -190,22 +207,27 @@ bool YAML::convert<Constant>::decode(const YAML::Node& node, Constant& rhs) {
return true;
}
YAML::Node YAML::convert<Probability>::encode(const Probability& rhs) {
YAML::Node YAML::convert<Property>::encode(const Property& rhs) {
YAML::Node node;
node.push_back(rhs.probability_);
node.push_back(rhs.property);
node.push_back(rhs.value_);
return node;
}
bool YAML::convert<Probability>::decode(const YAML::Node& node, Probability& rhs) {
if (!node.IsDefined() || !node["probability"] || !node["value"]) {
bool YAML::convert<Property>::decode(const YAML::Node& node, Property& rhs) {
if (!node.IsDefined() || !node["property"] || !node["value"]) {
return false;
}
rhs.probability_ = node["probability"].as<std::string>();
rhs.property = node["property"].as<std::string>();
try {
rhs.value_ = node["value"].as<double>();
}
catch(const std::exception& e) {
rhs.value_str_ = node["value"].as<std::string>();
}
return true;
}
@ -215,7 +237,7 @@ const std::string Configuration::overwrite_identifier_{"; // Overwritten through
YamlConfigParseResult YamlConfigParser::parseConfiguration() {
std::vector<Configuration> configuration;
std::vector<Probability> probabilities;
std::vector<Property> properties;
try {
YAML::Node config = YAML::LoadFile(file_);
@ -238,8 +260,8 @@ YamlConfigParseResult YamlConfigParser::parseConfiguration() {
constants = config["constants"].as<std::vector<Constant>>();
}
if (config["probabilities"]) {
probabilities = config["probabilities"].as<std::vector<Probability>>();
if (config["properties"]) {
properties = config["properties"].as<std::vector<Property>>();
}
for (auto& label : labels) {
@ -249,8 +271,22 @@ YamlConfigParseResult YamlConfigParser::parseConfiguration() {
configuration.push_back({formula.createExpression(), formula.formula_ ,ConfigType::Formula, formula.overwrite_});
}
for (auto& module : modules) {
if (module.overwrite_module) {
Configuration config = Configuration(module.module_text_, "module " + module.module_ + "\n", ConfigType::Module, true, module.module_, {0}, "endmodule");
configuration.push_back(config);
continue;
}
for (auto& command : module.commands_) {
configuration.push_back({command.createExpression(), command.action_, ConfigType::Module, command.overwrite_, module.module_, command.indexes_});
Configuration config;
if (!command.guard_.empty() && !command.action_.empty() && command.update_.empty()) {
config = Configuration(" " + command.guard_, command.action_, ConfigType::GuardOnly, true, module.module_, command.indexes_, "->");
} else if (!command.update_.empty() && !command.action_.empty() && command.guard_.empty()) {
config = Configuration( " " + command.update_, command.action_, ConfigType::UpdateOnly, true, module.module_, command.indexes_, ";");
} else {
config = Configuration(command.createExpression(), command.action_, ConfigType::Module, command.overwrite_, module.module_, command.indexes_);
}
configuration.push_back(config);
}
}
for (auto& constant : constants) {
@ -264,5 +300,5 @@ YamlConfigParseResult YamlConfigParser::parseConfiguration() {
std::cout << "while parsing configuration " << file_ << std::endl;
}
return YamlConfigParseResult(configuration, probabilities);
return YamlConfigParseResult(configuration, properties);
}

33
util/ConfigYaml.h
View File

@ -11,6 +11,8 @@ enum class ConfigType : char {
Label = 'L',
Formula = 'F',
Module = 'M',
UpdateOnly = 'U',
GuardOnly = 'G',
Constant = 'C'
};
@ -22,6 +24,7 @@ struct Configuration
std::string module_ {};
std::string expression_{};
std::string identifier_{};
std::string end_identifier_{};
std::vector<int> indexes_{0};
ConfigType type_ {ConfigType::Label};
@ -33,7 +36,8 @@ struct Configuration
, ConfigType type
, bool overwrite = false
, std::string module = ""
, std::vector<int> indexes = {0}) : expression_(expression), identifier_(identifier), type_(type), overwrite_(overwrite), module_{module}, indexes_(indexes) {}
, std::vector<int> indexes = {0}
, std::string end_identifier = {";"}) : expression_(expression), identifier_(identifier), type_(type), overwrite_(overwrite), module_{module}, indexes_(indexes), end_identifier_{end_identifier} {}
~Configuration() = default;
Configuration(const Configuration&) = default;
@ -44,15 +48,16 @@ struct Configuration
}
};
struct Probability {
Probability() = default;
Probability(const Probability&) = default;
~Probability() = default;
struct Property {
Property() = default;
Property(const Property&) = default;
~Property() = default;
std::string probability_;
std::string property;
double value_;
std::string value_str_;
friend std::ostream& operator <<(std::ostream& os, const Probability& property);
friend std::ostream& operator <<(std::ostream& os, const Property& property);
};
struct Constant {
@ -113,6 +118,8 @@ struct Module {
std::vector<Command> commands_;
std::string module_;
std::string module_text_;
bool overwrite_module{false};
friend std::ostream& operator << (std::ostream& os, const Module& module);
};
@ -150,20 +157,20 @@ struct YAML::convert<Constant> {
};
template<>
struct YAML::convert<Probability> {
static YAML::Node encode(const Probability& rhs);
static bool decode(const YAML::Node& node, Probability& rhs);
struct YAML::convert<Property> {
static YAML::Node encode(const Property& rhs);
static bool decode(const YAML::Node& node, Property& rhs);
};
struct YamlConfigParseResult {
YamlConfigParseResult(std::vector<Configuration> configurations, std::vector<Probability> probabilities)
: configurations_(configurations), probabilities_(probabilities) {}
YamlConfigParseResult(std::vector<Configuration> configurations, std::vector<Property> probabilities)
: configurations_(configurations), properties_(probabilities) {}
~YamlConfigParseResult() = default;
YamlConfigParseResult(const YamlConfigParseResult&) = default;
std::vector<Configuration> configurations_;
std::vector<Probability> probabilities_;
std::vector<Property> properties_;
};
struct YamlConfigParser {

27
util/Grid.cpp
View File

@ -15,6 +15,10 @@ Grid::Grid(cells gridCells, cells background, const std::map<coordinates, float>
std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyEast), [](cell c) { return c.type == Type::SlipperyEast; });
std::copy_if(background.begin(), background.end(), std::back_inserter(slipperySouth), [](cell c) { return c.type == Type::SlipperySouth; });
std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyWest), [](cell c) { return c.type == Type::SlipperyWest; });
std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyNorthWest), [](cell c) { return c.type == Type::SlipperyNorthWest; });
std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyNorthEast), [](cell c) { return c.type == Type::SlipperyNorthEast; });
std::copy_if(background.begin(), background.end(), std::back_inserter(slipperySouthWest), [](cell c) { return c.type == Type::SlipperySouthWest; });
std::copy_if(background.begin(), background.end(), std::back_inserter(slipperySouthEast), [](cell c) { return c.type == Type::SlipperySouthEast; });
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(lockedDoors), [](cell c) { return c.type == Type::LockedDoor; });
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(unlockedDoors), [](cell c) { return c.type == Type::Door; });
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(goals), [](cell c) { return c.type == Type::Goal; });
@ -62,7 +66,7 @@ Grid::Grid(cells gridCells, cells background, const std::map<coordinates, float>
}
}
if(adversaries.empty()) {
if (adversaries.empty()) {
modelType = prism::ModelType::MDP;
} else {
modelType = prism::ModelType::SMG;
@ -111,14 +115,26 @@ void Grid::applyOverwrites(std::string& str, std::vector<Configuration>& configu
search = "label " + config.identifier_;
} else if (config.type_ == ConfigType::Module) {
search = config.identifier_;
} else if (config.type_ == ConfigType::UpdateOnly) {
search = config.identifier_;
} else if (config.type_ == ConfigType::GuardOnly) {
search = config.identifier_;
}
else if (config.type_ == ConfigType::Constant) {
search = config.identifier_;
}
auto iter = boost::find_nth(str, search, index);
auto end_identifier = config.end_identifier_;
start_pos = std::distance(str.begin(), iter.begin());
size_t end_pos = str.find(';', start_pos) + 1;
size_t end_pos = str.find(end_identifier, start_pos);
if (config.type_ == ConfigType::GuardOnly || config.type_ == ConfigType::Module) {
start_pos += search.length();
} else if (config.type_ == ConfigType::UpdateOnly) {
start_pos = str.find("->", start_pos) + 2;
}
if (end_pos != std::string::npos && end_pos != 0) {
std::string expression = config.expression_;
@ -145,7 +161,7 @@ void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configurat
std::map<std::string, cells> wallRestrictions = {{"North", northRestriction}, {"East", eastRestriction}, {"South", southRestriction}, {"West", westRestriction}};
std::map<std::string, cells> slipperyTiles = {{"North", slipperyNorth}, {"East", slipperyEast}, {"South", slipperySouth}, {"West", slipperyWest}};
std::map<std::string, cells> slipperyTiles = {{"North", slipperyNorth}, {"East", slipperyEast}, {"South", slipperySouth}, {"West", slipperyWest}, {"NorthWest", slipperyNorthWest}, {"NorthEast", slipperyNorthEast},{"SouthWest", slipperySouthWest},{"SouthEast", slipperySouthEast}};
std::vector<AgentName> agentNames;
std::transform(agentNameAndPositionMap.begin(),
@ -177,3 +193,8 @@ void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configurat
// modules.printConfiguration(os, configuration);
//}
}
void Grid::setModelType(prism::ModelType type)
{
modelType = type;
}

6
util/Grid.h
View File

@ -22,6 +22,8 @@ class Grid {
void printToPrism(std::ostream &os, std::vector<Configuration>& configuration);
void applyOverwrites(std::string& str, std::vector<Configuration>& configuration);
void setModelType(prism::ModelType type);
std::array<bool, 8> getWalkableDirOf8Neighborhood(cell c);
friend std::ostream& operator<<(std::ostream& os, const Grid &grid);
@ -44,6 +46,10 @@ class Grid {
cells slipperyEast;
cells slipperySouth;
cells slipperyWest;
cells slipperyNorthWest;
cells slipperyNorthEast;
cells slipperySouthWest;
cells slipperySouthEast;
cells lockedDoors;
cells unlockedDoors;
cells boxes;

5
util/MinigridGrammar.h
View File

@ -66,6 +66,10 @@ template <typename It>
("e", Type::SlipperyEast)
("s", Type::SlipperySouth)
("w", Type::SlipperyWest)
("a", Type::SlipperyNorthWest)
("b", Type::SlipperyNorthEast)
("c", Type::SlipperySouthWest)
("d", Type::SlipperySouthEast)
("X", Type::Agent)
("Z", Type::Adversary);
color_.add
@ -74,6 +78,7 @@ template <typename It>
("B", Color::Blue)
("P", Color::Purple)
("Y", Color::Yellow)
("W", Color::White)
(" ", Color::None);
cell_ = type_ > color_;

36
util/PrismFormulaPrinter.cpp
View File

@ -4,6 +4,7 @@
#include <string>
#include <algorithm>
std::string oneOffToString(const int &offset) {
return offset != 0 ? ( offset == 1 ? "+1" : "-1" ) : "";
}
@ -71,7 +72,10 @@ namespace prism {
for(const auto& [direction, cells] : slipperyTiles) {
printIsOnFormula(agentName, "Slippery", cells, direction);
}
std::vector<std::string> allSlipperyDirections = {agentName + "IsOnSlipperyNorth", agentName + "IsOnSlipperyEast", agentName + "IsOnSlipperySouth", agentName + "IsOnSlipperyWest"};
std::vector<std::string> allSlipperyDirections;
for(const auto &[slipperyType, _] : slipperyTiles) {
allSlipperyDirections.push_back(agentName + "IsOnSlippery" + slipperyType);
}
os << buildFormula(agentName + "IsOnSlippery", vectorToDisjunction(allSlipperyDirections));
for(const auto& [direction, relativePosition] : getRelativeSurroundingCells()) {
@ -104,6 +108,8 @@ namespace prism {
if(conditionalMovementRestrictions.size() > 0) {
os << buildFormula(agentName + "CannotMoveConditionally", vectorToDisjunction(conditionalMovementRestrictions));
}
if(portableObjects.size() > 0) {
os << buildFormula(agentName + "IsCarrying", vectorToDisjunction(portableObjects));
}
}
@ -158,20 +164,20 @@ namespace prism {
}
void PrismFormulaPrinter::printInitStruct() {
os << "init\n";
bool first = true;
for(auto const [a, coordinates] : agentNameAndPositionMap) {
if(first) first = false;
else os << " & ";
os << "(col"+a+"="+std::to_string(coordinates.first)+"&row"+a+"="+std::to_string(coordinates.second)+" & ";
os << "(view"+a+"=0|view"+a+"=1|view"+a+"=2|view"+a+"=3) ";
if(faulty) os << " & previousAction"+a+"="+std::to_string(NOFAULT);
os << ")";
}
for(auto const key : keys) {
std::string identifier = capitalize(key.getColor()) + key.getType();
os << " & (col"+identifier+"="+std::to_string(key.column)+"&row"+identifier+"="+std::to_string(key.row)+"&"+identifier+"PickedUp=false) ";
}
os << "init\n true\n";
//bool first = true;
//for(auto const [a, coordinates] : agentNameAndPositionMap) {
// if(first) first = false;
// else os << " & ";
// os << "(col"+a+"="+std::to_string(coordinates.first)+"&row"+a+"="+std::to_string(coordinates.second)+" & ";
// os << "(view"+a+"=0|view"+a+"=1|view"+a+"=2|view"+a+"=3) ";
// if(faulty) os << " & previousAction"+a+"="+std::to_string(NOFAULT);
// os << ")";
//}
//for(auto const key : keys) {
// std::string identifier = capitalize(key.getColor()) + key.getType();
// os << " & (col"+identifier+"="+std::to_string(key.column)+"&row"+identifier+"="+std::to_string(key.row)+"&"+identifier+"PickedUp=false) ";
//}
os << "endinit\n\n";
}

174
util/PrismModulesPrinter.cpp
View File

@ -2,6 +2,7 @@
#include <map>
#include <string>
#include <stdexcept>
std::string northUpdate(const AgentName &a) { return "(row"+a+"'=row"+a+"-1)"; }
@ -143,21 +144,21 @@ namespace prism {
}
void PrismModulesPrinter::printLockedDoorActions(const std::string &agentName, const std::string &identifier) {
std::string actionName = "[" + agentName + "_unlock_" + identifier + "]";
std::string actionName = "[" + agentName + "_toggle_" + identifier + "]";
agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
os << " " << actionName << " !" << identifier << "Open -> (" << identifier << "Open'=true);\n";
actionName = "[" + agentName + "_close_" + identifier + "]";
actionName = "[" + agentName + "_toggle_" + identifier + "]";
agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
os << " " << actionName << " " << identifier << "Open -> (" << identifier << "Open'=false);\n";
}
void PrismModulesPrinter::printUnlockedDoorActions(const std::string &agentName, const std::string &identifier) {
std::string actionName = "[" + agentName + "_open_" + identifier + "]";
std::string actionName = "[" + agentName + "_toggle_" + identifier + "]";
agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
os << " !" << identifier << "Open -> (" << identifier << "Open'=true);\n";
actionName = "[" + agentName + "_close_" + identifier + "]";
os << " " << actionName << " !" << identifier << "Open -> (" << identifier << "Open'=true);\n";
actionName = "[" + agentName + "_toggle_" + identifier + "]";
agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
os << " " << agentName << " " << identifier << "Open -> (" << identifier << "Open'=false);\n";
os << " " << actionName << " " << identifier << "Open -> (" << identifier << "Open'=false);\n";
}
void PrismModulesPrinter::printRobotModule(const AgentName &agentName, const coordinates &initialPosition) {
@ -187,13 +188,13 @@ namespace prism {
printPortableObjectActionsForRobot(agentName, identifier);
}
printNonMovementActionsForRobot(agentName);
//printNonMovementActionsForRobot(agentName);
os << "\n" << actionStream.str();
actionStream.str(std::string());
if(agentNameAndPositionMap.size() > 1 && agentName == "Agent") printDoneActions(agentName);
if(agentNameAndPositionMap.size() > 1 && agentName == "Agent" && anyGoals) printDoneActions(agentName);
os << "endmodule\n\n";
}
@ -209,14 +210,14 @@ namespace prism {
}
void PrismModulesPrinter::printUnlockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier) {
actionStream << " [" << agentName << "_open_" << identifier << "] " << agentName << "CannotMove" << identifier << " -> true;\n";
actionStream << " [" << agentName << "_close_" << identifier << "] " << agentName << "IsNextTo" << identifier << " -> true;\n";
actionStream << " [" << agentName << "_toggle_" << identifier << "] " << agentName << "CannotMove" << identifier << " -> true;\n";
actionStream << " [" << agentName << "_toggle_" << identifier << "] " << agentName << "IsNextTo" << identifier << " -> true;\n";
actionStream << "\n";
}
void PrismModulesPrinter::printLockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier, const std::string &key) {
actionStream << " [" << agentName << "_unlock_" << identifier << "] " << agentName << "CannotMove" << identifier << " & " << agentName << "Carrying" << key << " -> true;\n";
actionStream << " [" << agentName << "_close_" << identifier << "] " << agentName << "IsNextTo" << identifier << " & " << agentName << "Carrying" << key << " -> true;\n";
actionStream << " [" << agentName << "_toggle_" << identifier << "] " << agentName << "CannotMove" << identifier << " & " << agentName << "Carrying" << key << " -> true;\n";
actionStream << " [" << agentName << "_toggle_" << identifier << "] " << agentName << "IsNextTo" << identifier << " & " << agentName << "Carrying" << key << " -> true;\n";
actionStream << "\n";
}
@ -248,9 +249,9 @@ namespace prism {
std::string guard = " " + actionName + " " + viewVariable(a, viewDirection);
if(slipperyBehaviour()) guard += " & !" + a + "IsOnSlippery";
if(anyLava) guard += " & !" + a + "IsOnLava";
if(anyGoals) guard += " & !" + a + "IsOnGoal";
if(anyGoals && a == "Agent") guard += " & !" + a + "IsOnGoal";
guard += " & !" + a + "CannotMove" + direction + "Wall";
if(anyPortableObject()) guard += " & !" + a + "CannotMoveConditionally";
if(anyPortableObject() || !lockedDoors.empty() || !unlockedDoors.empty()) guard += " & !" + a + "CannotMoveConditionally";
guard += " -> ";
return guard;
}
@ -298,6 +299,22 @@ namespace prism {
printSlipperyMovementActionsForWest(a) ;
printSlipperyTurnActionsForWest(a);
}
if(!slipperyTiles.at("NorthWest").empty()) {
printSlipperyMovementActionsForNorthWest(a);
printSlipperyTurnActionsForNorthWest(a);
}
if(!slipperyTiles.at("NorthEast").empty()) {
printSlipperyMovementActionsForNorthEast(a);
printSlipperyTurnActionsForNorthEast(a);
}
if(!slipperyTiles.at("SouthWest").empty()) {
printSlipperyMovementActionsForSouthWest(a);
printSlipperyTurnActionsForSouthWest(a);
}
if(!slipperyTiles.at("SouthWest").empty()) {
printSlipperyMovementActionsForSouthWest(a);
printSlipperyTurnActionsForSouthWest(a);
}
}
void PrismModulesPrinter::printSlipperyMovementActionsForNorth(const AgentName &a) {
@ -397,44 +414,117 @@ namespace prism {
}
void PrismModulesPrinter::printSlipperyTurnActionsForNorth(const AgentName &a) {
actionStream << printSlipperyTurnGuard(a, "right", RIGHT, {"!"+a+"CannotSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, northUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "right", RIGHT, { a+"CannotSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "right", "North", RIGHT, {"!"+a+"CannotSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, northUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "right", "North", RIGHT, { a+"CannotSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!"+a+"CannotSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, northUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!"+a+"CannotSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, northUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", LEFT, { a+"CannotSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", LEFT, { a+"CannotSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, {"!"+a+"CannotSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, northUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, {"!"+a+"CannotSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, northUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, { a+"CannotSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, { a+"CannotSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n";
}
void PrismModulesPrinter::printSlipperyTurnActionsForEast(const AgentName &a) {
actionStream << printSlipperyTurnGuard(a, "right", RIGHT, {"!"+a+"CannotSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, eastUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "right", RIGHT, { a+"CannotSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "right", "East", RIGHT, {"!"+a+"CannotSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, eastUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "right", "East", RIGHT, { a+"CannotSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!"+a+"CannotSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, eastUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!"+a+"CannotSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, eastUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", LEFT, { a+"CannotSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", LEFT, { a+"CannotSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, {"!"+a+"CannotSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, eastUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, {"!"+a+"CannotSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, eastUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, { a+"CannotSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, { a+"CannotSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n";
}
void PrismModulesPrinter::printSlipperyTurnActionsForSouth(const AgentName &a) {
actionStream << printSlipperyTurnGuard(a, "right", RIGHT, {"!"+a+"CannotSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, southUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "right", RIGHT, { a+"CannotSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "right", "South", RIGHT, {"!"+a+"CannotSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, southUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "right", "South", RIGHT, { a+"CannotSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!"+a+"CannotSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, southUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!"+a+"CannotSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, southUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", LEFT, { a+"CannotSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", LEFT, { a+"CannotSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, {"!"+a+"CannotSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, southUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, {"!"+a+"CannotSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, southUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, { a+"CannotSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, { a+"CannotSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n";
}
void PrismModulesPrinter::printSlipperyTurnActionsForWest(const AgentName &a) {
actionStream << printSlipperyTurnGuard(a, "right", RIGHT, {"!"+a+"CannotSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, westUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "right", RIGHT, { a+"CannotSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "right", "West", RIGHT, {"!"+a+"CannotSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, westUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "right", "West", RIGHT, { a+"CannotSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, {"!"+a+"CannotSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, westUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, {"!"+a+"CannotSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, westUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, { a+"CannotSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, { a+"CannotSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n";
}
void PrismModulesPrinter::printSlipperyMovementActionsForNorthWest(const AgentName &a) { throw std::logic_error("The logic for SlipperyNorthWest tiles is not yet implemented."); }
void PrismModulesPrinter::printSlipperyTurnActionsForNorthWest(const AgentName &a){ throw std::logic_error("The logic for SlipperyNorthWest tiles is not yet implemented."); }
void PrismModulesPrinter::printSlipperyMovementActionsForNorthEast(const AgentName &a) {
actionStream << printSlipperyMovementGuard(a, "NorthEast", 0, {"!"+a+"CannotSlipNorthEast", "!"+a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "", {{probIntended, eastUpdate(a)}, {1-probIntended, northUpdate(a)+"&"+eastUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 0, {"!"+a+"CannotSlipNorthEast", a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "", {{1, northUpdate(a)+"&"+eastUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 0, { a+"CannotSlipNorthEast", "!"+a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "", {{1, eastUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 0, { a+"CannotSlipNorthEast", a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "", {{1, "true"}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 3, {"!"+a+"CannotSlipNorthEast", "!"+a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "", {{probIntended, northUpdate(a)}, {1-probIntended, eastUpdate(a)+"&"+northUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 3, {"!"+a+"CannotSlipNorthEast", a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "", {{1, northUpdate(a)+"&"+eastUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 3, { a+"CannotSlipNorthEast", "!"+a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "", {{1, northUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 3, { a+"CannotSlipNorthEast", a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "", {{1, "true"}}) << ";\n";
float pd3 = (1 - probIntended) / 3;
float pi3 = probIntended;
float sum2 = probIntended + 2 * (1 - probIntended)/3;
float pd2 = (1 - probIntended) / sum2;
float pi2 = probIntended / sum2;
float sum1 = probIntended + (1 - probIntended)/3;
float pd1 = (1 - probIntended) / sum1;
float pi1 = probIntended / sum1;
actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, {"!"+a+"CannotSlipNorthEast", "!"+a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{pi3, southUpdate(a)}, {pd3, northUpdate(a)+"&"+eastUpdate(a)}, {pd3, eastUpdate(a)}, {pd3, southUpdate(a)+"&"+eastUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, {"!"+a+"CannotSlipNorthEast", "!"+a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{1/3.f, northUpdate(a)+"&"+eastUpdate(a)}, {1/3.f, eastUpdate(a)}, {1/3.f, southUpdate(a)+"&"+eastUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, {"!"+a+"CannotSlipNorthEast", "!"+a+"CannotSlipEast", a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{pi1, southUpdate(a)}, {pd2, northUpdate(a)+"&"+eastUpdate(a)}, {pd2, eastUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, {"!"+a+"CannotSlipNorthEast", "!"+a+"CannotSlipEast", a+"CannotSlipSouthEast", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{1/2.f, northUpdate(a)+"&"+eastUpdate(a)}, {1/2.f, eastUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, {"!"+a+"CannotSlipNorthEast", a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{pi1, southUpdate(a)}, {pd2, northUpdate(a)+"&"+eastUpdate(a)}, {pd2, southUpdate(a)+"&"+eastUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, {"!"+a+"CannotSlipNorthEast", a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{1/2.f, northUpdate(a)+"&"+eastUpdate(a)}, {1/2.f, southUpdate(a)+"&"+eastUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, {"!"+a+"CannotSlipNorthEast", a+"CannotSlipEast", a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{pi1, southUpdate(a)}, {pd1, northUpdate(a)+"&"+eastUpdate(a) }}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, {"!"+a+"CannotSlipNorthEast", a+"CannotSlipEast", a+"CannotSlipSouthEast", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{1, northUpdate(a)+"&"+eastUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, { a+"CannotSlipNorthEast", "!"+a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{pi1, southUpdate(a)}, {pd2, eastUpdate(a)}, {pd2, southUpdate(a)+"&"+eastUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, { a+"CannotSlipNorthEast", "!"+a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{1/2.f, eastUpdate(a)}, {1/2.f, southUpdate(a)+"&"+eastUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, { a+"CannotSlipNorthEast", "!"+a+"CannotSlipEast", a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{pi1, southUpdate(a)}, {pd1, eastUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, { a+"CannotSlipNorthEast", "!"+a+"CannotSlipEast", a+"CannotSlipSouthEast", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{1, eastUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, { a+"CannotSlipNorthEast", a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{pi1, southUpdate(a)}, {pd1, southUpdate(a)+"&"+eastUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, { a+"CannotSlipNorthEast", a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{1, southUpdate(a)+"&"+eastUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, { a+"CannotSlipNorthEast", a+"CannotSlipEast", a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{1, southUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, { a+"CannotSlipNorthEast", a+"CannotSlipEast", a+"CannotSlipSouthEast", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{1, "true"}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipNorthWest", "!"+a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{pi3, westUpdate(a)}, {pd3, northUpdate(a)+"&"+westUpdate(a)}, {pd3, northUpdate(a)}, {pd3, northUpdate(a)+"&"+eastUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipNorthWest", "!"+a+"CannotSlipNorth", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{pi2, westUpdate(a)}, {pd2, northUpdate(a)+"&"+westUpdate(a)}, {pd2, northUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipNorthWest", a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{pi2, westUpdate(a)}, {pd2, northUpdate(a)+"&"+westUpdate(a)}, {pd2, northUpdate(a)+"&"+eastUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipNorthWest", a+"CannotSlipNorth", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{pi1, westUpdate(a)}, {pd1, northUpdate(a)+"&"+westUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, {"!"+a+"CannotSlipWest", a+"CannotSlipNorthWest", "!"+a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{pi2, westUpdate(a)}, {pd2, northUpdate(a)}, {pd2, northUpdate(a)+"&"+eastUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, {"!"+a+"CannotSlipWest", a+"CannotSlipNorthWest", "!"+a+"CannotSlipNorth", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{pi1, westUpdate(a)}, {pd1, northUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, {"!"+a+"CannotSlipWest", a+"CannotSlipNorthWest", a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{pi1, westUpdate(a)}, {pd1, northUpdate(a)+"&"+eastUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, {"!"+a+"CannotSlipWest", a+"CannotSlipNorthWest", a+"CannotSlipNorth", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{1, westUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, { a+"CannotSlipWest", "!"+a+"CannotSlipNorthWest", "!"+a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{1/3.f, northUpdate(a)+"&"+westUpdate(a)}, {1/3.f, northUpdate(a)}, {1/3.f, northUpdate(a)+"&"+eastUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, { a+"CannotSlipWest", "!"+a+"CannotSlipNorthWest", "!"+a+"CannotSlipNorth", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{1/2.f, northUpdate(a)+"&"+westUpdate(a)}, {1/2.f, northUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, { a+"CannotSlipWest", "!"+a+"CannotSlipNorthWest", a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{1/2.f, northUpdate(a)+"&"+westUpdate(a)}, {1/2.f, northUpdate(a)+"&"+eastUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, { a+"CannotSlipWest", "!"+a+"CannotSlipNorthWest", a+"CannotSlipNorth", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{1, northUpdate(a)+"&"+westUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, { a+"CannotSlipWest", a+"CannotSlipNorthWest", "!"+a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{1/2.f, northUpdate(a)}, {1/2.f, northUpdate(a)+"&"+eastUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, { a+"CannotSlipWest", a+"CannotSlipNorthWest", "!"+a+"CannotSlipNorth", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{1, northUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, { a+"CannotSlipWest", a+"CannotSlipNorthWest", a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{1, northUpdate(a)+"&"+eastUpdate(a)}}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, { a+"CannotSlipWest", a+"CannotSlipNorthWest", a+"CannotSlipNorth", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{1, "true"}}) << ";\n";
}
void PrismModulesPrinter::printSlipperyTurnActionsForNorthEast(const AgentName &a) {
actionStream << printSlipperyTurnGuard(a, "right", "NorthEast", RIGHT, {}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "NorthEast", LEFT, {}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "NorthEast", LEFT, {}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n";
}
void PrismModulesPrinter::printSlipperyMovementActionsForSouthWest(const AgentName &a){ throw std::logic_error("The logic for SlipperySouthWest tiles is not yet implemented."); }
void PrismModulesPrinter::printSlipperyTurnActionsForSouthWest(const AgentName &a){ throw std::logic_error("The logic for SlipperySouthWest tiles is not yet implemented."); }
void PrismModulesPrinter::printSlipperyMovementActionsForSouthEast(const AgentName &a){ throw std::logic_error("The logic for SlipperySouthEast tiles is not yet implemented."); }
void PrismModulesPrinter::printSlipperyTurnActionsForSouthEast(const AgentName &a){ throw std::logic_error("The logic for SlipperySouthEast tiles is not yet implemented."); }
actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!"+a+"CannotSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, westUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!"+a+"CannotSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, westUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", LEFT, { a+"CannotSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", LEFT, { a+"CannotSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n";
}
std::string PrismModulesPrinter::printSlipperyMovementGuard(const AgentName &a, const std::string &direction, const ViewDirection &viewDirection, const std::vector<std::string> &guards) {
std::string actionName = "[" + a + "_move_" + viewDirectionToString.at(viewDirection) + "]";
@ -446,10 +536,10 @@ namespace prism {
return updatesToString(u);
}
std::string PrismModulesPrinter::printSlipperyTurnGuard(const AgentName &a, const std::string &direction, const ActionId &actionId, const std::vector<std::string> &guards, const std::string &cond) {
std::string PrismModulesPrinter::printSlipperyTurnGuard(const AgentName &a, const std::string &direction, const std::string &tiltDirection, const ActionId &actionId, const std::vector<std::string> &guards, const std::string &cond) {
std::string actionName = "[" + a + "_turn_" + direction + "]";
agentNameActionMap.at(a).insert({actionId, actionName});
return " " + actionName + " " + a + "IsOnSlippery & " + buildConjunction(a, guards) + " & " + cond + " -> ";
return " " + actionName + " " + a + "IsOnSlippery" + tiltDirection + " & " + buildConjunction(a, guards) + " & " + cond + " -> ";
}
std::string PrismModulesPrinter::printSlipperyTurnUpdate(const AgentName &a, const updates &u) {
@ -502,7 +592,7 @@ namespace prism {
else os << ", ";
os << actionName;
}
if(agentName == "Agent") os << ", [Agent_on_goal]";
if(agentName == "Agent" && anyGoals) os << ", [Agent_on_goal]";
os << "\nendplayer\n";
}

10
util/PrismModulesPrinter.h
View File

@ -48,6 +48,14 @@ namespace prism {
void printSlipperyTurnActionsForEast(const AgentName &a);
void printSlipperyTurnActionsForSouth(const AgentName &a);
void printSlipperyTurnActionsForWest(const AgentName &a);
void printSlipperyMovementActionsForNorthWest(const AgentName &a);
void printSlipperyTurnActionsForNorthWest(const AgentName &a);
void printSlipperyMovementActionsForNorthEast(const AgentName &a);
void printSlipperyTurnActionsForNorthEast(const AgentName &a);
void printSlipperyMovementActionsForSouthWest(const AgentName &a);
void printSlipperyTurnActionsForSouthWest(const AgentName &a);
void printSlipperyMovementActionsForSouthEast(const AgentName &a);
void printSlipperyTurnActionsForSouthEast(const AgentName &a);
std::string printMovementGuard(const AgentName &a, const std::string &direction, const size_t &viewDirection);
std::string printMovementUpdate(const AgentName &a, const update &update) const;
@ -55,7 +63,7 @@ namespace prism {
std::string printTurnUpdate(const AgentName &a, const update &u, const ActionId &actionId) const;
std::string printSlipperyMovementGuard(const AgentName &a, const std::string &direction, const ViewDirection &viewDirection, const std::vector<std::string> &guards);
std::string printSlipperyMovementUpdate(const AgentName &a, const std::string &direction, const updates &u) const;
std::string printSlipperyTurnGuard(const AgentName &a, const std::string &direction, const ActionId &actionId, const std::vector<std::string> &guards, const std::string &cond);
std::string printSlipperyTurnGuard(const AgentName &a, const std::string &direction, const std::string &tiltDirection, const ActionId &actionId, const std::vector<std::string> &guards, const std::string &cond);
std::string printSlipperyTurnUpdate(const AgentName &a, const updates &u);
void printFaultyMovementModule(const AgentName &a);

7
util/cell.h
View File

@ -23,7 +23,11 @@ enum class Type : char {
SlipperyNorth = 'n',
SlipperySouth = 's',
SlipperyEast = 'e',
SlipperyWest = 'w'
SlipperyWest = 'w',
SlipperyNorthWest = 'a',
SlipperyNorthEast = 'b',
SlipperySouthWest = 'c',
SlipperySouthEast = 'd'
};
enum class Color : char {
Red = 'R',
@ -31,6 +35,7 @@ enum class Color : char {
Blue = 'B',
Purple = 'P',
Yellow = 'Y',
White = 'W',
//Grey = 'G',
None = ' '
};

Write Preview
Loading…
Cancel
Save