Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[issue1146] Validate SAS file #227

Draft
wants to merge 12 commits into
base: main
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from 8 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions src/search/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -134,6 +134,7 @@ create_fast_downward_library(
utils/countdown_timer
utils/exceptions
utils/hash
utils/input_file_parser
utils/language
utils/logging
utils/markup
Expand Down
218 changes: 127 additions & 91 deletions src/search/tasks/root_task.cc
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@

#include "../plugins/plugin.h"
#include "../utils/collections.h"
#include "../utils/input_file_parser.h"
#include "../utils/timer.h"

#include <algorithm>
Expand All @@ -28,7 +29,7 @@ struct ExplicitVariable {
int axiom_layer;
int axiom_default_value;

explicit ExplicitVariable(istream &in);
explicit ExplicitVariable(utils::InputFileParser &file_parser);
};


Expand All @@ -47,8 +48,9 @@ struct ExplicitOperator {
string name;
bool is_an_axiom;

void read_pre_post(istream &in);
ExplicitOperator(istream &in, bool is_an_axiom, bool use_metric);
void read_pre_post(utils::InputFileParser &in);
void read_axiom(utils::InputFileParser &in);
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should this (and read_pre_post) be private?

ExplicitOperator(utils::InputFileParser &in, bool is_an_axiom, bool use_metric);
tanjaschindler marked this conversation as resolved.
Show resolved Hide resolved
};


Expand Down Expand Up @@ -125,6 +127,12 @@ static void check_facts(const vector<FactPair> &facts, const vector<ExplicitVari
}
}

static void check_facts(const set<FactPair> &facts, const vector<ExplicitVariable> &variables) {
tanjaschindler marked this conversation as resolved.
Show resolved Hide resolved
for (FactPair fact : facts) {
check_fact(fact, variables);
}
}

static void check_facts(const ExplicitOperator &action, const vector<ExplicitVariable> &variables) {
check_facts(action.preconditions, variables);
for (const ExplicitEffect &eff : action.effects) {
Expand All @@ -133,44 +141,35 @@ static void check_facts(const ExplicitOperator &action, const vector<ExplicitVar
}
}

static void check_magic(istream &in, const string &magic) {
string word;
in >> word;
if (word != magic) {
cerr << "Failed to match magic word '" << magic << "'." << endl
<< "Got '" << word << "'." << endl;
if (magic == "begin_version") {
cerr << "Possible cause: you are running the planner "
<< "on a translator output file from " << endl
<< "an older version." << endl;
}
utils::exit_with(ExitCode::SEARCH_INPUT_ERROR);
}
}

static vector<FactPair> read_facts(istream &in) {
int count;
in >> count;
static vector<FactPair> read_facts(utils::InputFileParser &in, bool read_from_single_line) {
int count = read_from_single_line ? in.read_int("number of conditions")
tanjaschindler marked this conversation as resolved.
Show resolved Hide resolved
: in.read_line_int("number of conditions");
vector<FactPair> conditions;
conditions.reserve(count);
for (int i = 0; i < count; ++i) {
FactPair condition = FactPair::no_fact;
in >> condition.var >> condition.value;
condition.var = in.read_int("condition variable");
condition.value = in.read_int("condition value");
if (!read_from_single_line) {
in.confirm_end_of_line();
}
conditions.push_back(condition);
}
return conditions;
}

ExplicitVariable::ExplicitVariable(istream &in) {
check_magic(in, "begin_variable");
in >> name;
in >> axiom_layer;
in >> domain_size;
in >> ws;
ExplicitVariable::ExplicitVariable(utils::InputFileParser &file_parser) {
file_parser.read_magic_line("begin_variable");
name = file_parser.read_line("variable name");
axiom_layer = file_parser.read_line_int("variable axiom layer");
domain_size = file_parser.read_line_int("variable domain size");
if (domain_size < 1) {
file_parser.error("Domain size is less than 1, should be at least 1.");
}
fact_names.resize(domain_size);
for (int i = 0; i < domain_size; ++i)
getline(in, fact_names[i]);
check_magic(in, "end_variable");
fact_names[i] = file_parser.read_line("fact name");
file_parser.read_magic_line("end_variable");
}


Expand All @@ -179,84 +178,104 @@ ExplicitEffect::ExplicitEffect(
: fact(var, value), conditions(move(conditions)) {
}

void ExplicitOperator::read_pre_post(utils::InputFileParser &in) {
vector<FactPair> conditions = read_facts(in, true);
int var = in.read_int("variable affected by effect");
int value_pre = in.read_int("variable value precondition");
int value_post = in.read_int("variable value postcondition");
if (value_pre != -1) {
preconditions.emplace_back(var, value_pre);
}
in.confirm_end_of_line();
effects.emplace_back(var, value_post, move(conditions));
}

void ExplicitOperator::read_pre_post(istream &in) {
vector<FactPair> conditions = read_facts(in);
int var, value_pre, value_post;
in >> var >> value_pre >> value_post;
void ExplicitOperator::read_axiom(utils::InputFileParser &in) {
tanjaschindler marked this conversation as resolved.
Show resolved Hide resolved
vector<FactPair> conditions = read_facts(in, false);
int var = in.read_int("variable affected by axiom");
int value_pre = in.read_int("variable value precondition");
int value_post = in.read_int("variable value postcondition");
in.confirm_end_of_line();
if (value_pre != -1) {
preconditions.emplace_back(var, value_pre);
}
effects.emplace_back(var, value_post, move(conditions));
}

ExplicitOperator::ExplicitOperator(istream &in, bool is_an_axiom, bool use_metric)
ExplicitOperator::ExplicitOperator(utils::InputFileParser &in, bool is_an_axiom, bool use_metric)
: is_an_axiom(is_an_axiom) {
if (!is_an_axiom) {
check_magic(in, "begin_operator");
in >> ws;
getline(in, name);
preconditions = read_facts(in);
int count;
in >> count;
in.read_magic_line("begin_operator");
name = in.read_line("operator name");
preconditions = read_facts(in, false);
int count = in.read_line_int("number of operator effects");
effects.reserve(count);
for (int i = 0; i < count; ++i) {
read_pre_post(in);
}

int op_cost;
in >> op_cost;
int op_cost = in.read_line_int("operator cost");
cost = use_metric ? op_cost : 1;
check_magic(in, "end_operator");
in.read_magic_line("end_operator");
} else {
name = "<axiom>";
cost = 0;
check_magic(in, "begin_rule");
read_pre_post(in);
check_magic(in, "end_rule");
in.read_magic_line("begin_rule");
read_axiom(in);
in.read_magic_line("end_rule");
}
assert(cost >= 0);
}

static void read_and_verify_version(istream &in) {
int version;
check_magic(in, "begin_version");
in >> version;
check_magic(in, "end_version");
static void read_and_verify_version(utils::InputFileParser &in) {
in.set_context("version section");
tanjaschindler marked this conversation as resolved.
Show resolved Hide resolved
in.read_magic_line("begin_version");
int version = in.read_line_int("version number");
if (version != PRE_FILE_VERSION) {
cerr << "Expected translator output file version " << PRE_FILE_VERSION
<< ", got " << version << "." << endl
<< "Exiting." << endl;
utils::exit_with(ExitCode::SEARCH_INPUT_ERROR);
}
}

static bool read_metric(istream &in) {
bool use_metric;
check_magic(in, "begin_metric");
in >> use_metric;
check_magic(in, "end_metric");
in.read_magic_line("end_version");
}

static bool read_metric(utils::InputFileParser &in) {
in.set_context("metric_section");
in.read_magic_line("begin_metric");
string use_metric_string = in.read_line("use metric");
bool use_metric = false;
if (use_metric_string == "1") {
use_metric = true;
} else if (use_metric_string == "0") {
use_metric = false;
} else {
in.error("expected boolean");
tanjaschindler marked this conversation as resolved.
Show resolved Hide resolved
}
in.read_magic_line("end_metric");
return use_metric;
}

static vector<ExplicitVariable> read_variables(istream &in) {
int count;
in >> count;
static vector<ExplicitVariable> read_variables(utils::InputFileParser &file_parser) {
tanjaschindler marked this conversation as resolved.
Show resolved Hide resolved
file_parser.set_context("variable_section");
int count = file_parser.read_line_int("variable count");
if (count < 1) {
file_parser.error("Number of variables is less than 1, should be at least 1.");
tanjaschindler marked this conversation as resolved.
Show resolved Hide resolved
}
vector<ExplicitVariable> variables;
variables.reserve(count);
for (int i = 0; i < count; ++i) {
variables.emplace_back(in);
variables.emplace_back(file_parser);
}
return variables;
}

static vector<vector<set<FactPair>>> read_mutexes(istream &in, const vector<ExplicitVariable> &variables) {
static vector<vector<set<FactPair>>> read_mutexes(utils::InputFileParser &file_parser, const vector<ExplicitVariable> &variables) {
file_parser.set_context("mutex section");
vector<vector<set<FactPair>>> inconsistent_facts(variables.size());
for (size_t i = 0; i < variables.size(); ++i)
inconsistent_facts[i].resize(variables[i].domain_size);

int num_mutex_groups;
in >> num_mutex_groups;
int num_mutex_groups = file_parser.read_line_int("number of mutex groups");

/*
NOTE: Mutex groups can overlap, in which case the same mutex
Expand All @@ -266,18 +285,24 @@ static vector<vector<set<FactPair>>> read_mutexes(istream &in, const vector<Expl
aware of.
*/
for (int i = 0; i < num_mutex_groups; ++i) {
check_magic(in, "begin_mutex_group");
int num_facts;
in >> num_facts;
file_parser.read_magic_line("begin_mutex_group");
int num_facts = file_parser.read_line_int("number of facts in mutex group");
if (num_facts < 1) {
file_parser.error("Number of facts in mutex group is less than 1, should be at least 1.");
tanjaschindler marked this conversation as resolved.
Show resolved Hide resolved
}
vector<FactPair> invariant_group;
invariant_group.reserve(num_facts);
for (int j = 0; j < num_facts; ++j) {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Don't we already have a function that reads a list of facts? And doesn't it also need the check that there are no duplicate facts?

int var;
int value;
in >> var >> value;
int var = file_parser.read_int("variable number of mutex atom");
int value = file_parser.read_int("value of mutex atom");
file_parser.confirm_end_of_line();
invariant_group.emplace_back(var, value);
}
check_magic(in, "end_mutex_group");
file_parser.read_magic_line("end_mutex_group");
set<FactPair> invariant_group_set(invariant_group.begin(), invariant_group.end());
if (invariant_group_set.size() != invariant_group.size()) {
file_parser.error("Mutex group may not contain the same fact more than once.");
}
for (const FactPair &fact1 : invariant_group) {
for (const FactPair &fact2 : invariant_group) {
if (fact1.var != fact2.var) {
Expand All @@ -299,10 +324,11 @@ static vector<vector<set<FactPair>>> read_mutexes(istream &in, const vector<Expl
return inconsistent_facts;
}

static vector<FactPair> read_goal(istream &in) {
check_magic(in, "begin_goal");
vector<FactPair> goals = read_facts(in);
check_magic(in, "end_goal");
static vector<FactPair> read_goal(utils::InputFileParser &in) {
in.set_context("goal section");
in.read_magic_line("begin_goal");
vector<FactPair> goals = read_facts(in, false);
in.read_magic_line("end_goal");
if (goals.empty()) {
cerr << "Task has no goal condition!" << endl;
utils::exit_with(ExitCode::SEARCH_INPUT_ERROR);
Expand All @@ -311,10 +337,10 @@ static vector<FactPair> read_goal(istream &in) {
}

static vector<ExplicitOperator> read_actions(
istream &in, bool is_axiom, bool use_metric,
utils::InputFileParser &in, bool is_axiom, bool use_metric,
const vector<ExplicitVariable> &variables) {
int count;
in >> count;
in.set_context(is_axiom ? "axiom section" : "operator section");
tanjaschindler marked this conversation as resolved.
Show resolved Hide resolved
int count = in.read_line_int(is_axiom ? "number of axioms" : "number of operators");
vector<ExplicitOperator> actions;
actions.reserve(count);
for (int i = 0; i < count; ++i) {
Expand All @@ -325,28 +351,38 @@ static vector<ExplicitOperator> read_actions(
}

RootTask::RootTask(istream &in) {
read_and_verify_version(in);
bool use_metric = read_metric(in);
variables = read_variables(in);
utils::InputFileParser file(in);
tanjaschindler marked this conversation as resolved.
Show resolved Hide resolved
read_and_verify_version(file);
bool use_metric = read_metric(file);
variables = read_variables(file);
int num_variables = variables.size();

mutexes = read_mutexes(in, variables);
mutexes = read_mutexes(file, variables);
for (size_t i = 0; i < mutexes.size(); ++i) {
for (size_t j = 0; j < mutexes[i].size(); ++j) {
check_facts(mutexes[i][j], variables);
}
}

// TODO: Maybe we could move this into a separate function as well
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

sounds good

file.set_context("initial state section");
initial_state_values.resize(num_variables);
check_magic(in, "begin_state");
file.read_magic_line("begin_state");
for (int i = 0; i < num_variables; ++i) {
in >> initial_state_values[i];
initial_state_values[i] = file.read_line_int("initial state variable value");
}
check_magic(in, "end_state");
file.read_magic_line("end_state");

for (int i = 0; i < num_variables; ++i) {
check_fact(FactPair(i, initial_state_values[i]), variables);
variables[i].axiom_default_value = initial_state_values[i];
}

goals = read_goal(in);
goals = read_goal(file);
check_facts(goals, variables);
operators = read_actions(in, false, use_metric, variables);
axioms = read_actions(in, true, use_metric, variables);
operators = read_actions(file, false, use_metric, variables);
axioms = read_actions(file, true, use_metric, variables);
file.confirm_end_of_file();
/* TODO: We should be stricter here and verify that we
tanjaschindler marked this conversation as resolved.
Show resolved Hide resolved
have reached the end of "in". */

Expand Down
Loading
Loading