From 907e6f6da81f595e71a5fd1ad9ea1ce66a40aa89 Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Fri, 2 Feb 2024 12:06:25 +0100 Subject: [PATCH 1/6] [issue879] make invariant synthesis deterministic --- src/translate/invariant_finder.py | 10 +++++++--- src/translate/invariants.py | 9 ++++++--- 2 files changed, 13 insertions(+), 6 deletions(-) diff --git a/src/translate/invariant_finder.py b/src/translate/invariant_finder.py index 8aaee3fb99..a4b01dcfeb 100755 --- a/src/translate/invariant_finder.py +++ b/src/translate/invariant_finder.py @@ -13,7 +13,11 @@ class BalanceChecker: def __init__(self, task, reachable_action_params): - self.predicates_to_add_actions = defaultdict(set) + self.predicates_to_add_actions = defaultdict(dict) + # Conceptionally, predicates_to_add will store for each predicate the + # set of actions that have an add effect on the predicate. Since sets + # are not stable (introducing non-determinism in the algorithm), we + # store the actions as keys in a dictionary (which is stable). self.action_to_heavy_action = {} for act in task.actions: action = self.add_inequality_preconds(act, reachable_action_params) @@ -27,7 +31,7 @@ def __init__(self, task, reachable_action_params): too_heavy_effects.append(eff.copy()) if not eff.literal.negated: predicate = eff.literal.predicate - self.predicates_to_add_actions[predicate].add(action) + self.predicates_to_add_actions[predicate][action] = True if create_heavy_act: heavy_act = pddl.Action(action.name, action.parameters, action.num_external_parameters, @@ -38,7 +42,7 @@ def __init__(self, task, reachable_action_params): self.action_to_heavy_action[action] = heavy_act def get_threats(self, predicate): - return self.predicates_to_add_actions.get(predicate, set()) + return self.predicates_to_add_actions.get(predicate, dict()) def get_heavy_action(self, action): return self.action_to_heavy_action[action] diff --git a/src/translate/invariants.py b/src/translate/invariants.py index f91eb11a68..b5c30daaeb 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -324,10 +324,13 @@ def _get_cover_equivalence_conjunction(self, literal): def check_balance(self, balance_checker, enqueue_func): # Check balance for this hypothesis. - actions_to_check = set() + actions_to_check = dict() + # We will only use the keys of the dictionary. We do not use a set + # because it's not stable and introduces non-determinism in the + # invariance analysis. for part in self.parts: - actions_to_check |= balance_checker.get_threats(part.predicate) - for action in actions_to_check: + actions_to_check.update(balance_checker.get_threats(part.predicate)) + for action in actions_to_check.keys(): heavy_action = balance_checker.get_heavy_action(action) if self._operator_too_heavy(heavy_action): return False From a53f6d09519117e03abae00890afe981842e4dd6 Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Fri, 2 Feb 2024 12:13:33 +0100 Subject: [PATCH 2/6] [issue879] do not sort invariants (should not be necessary anymore) --- src/translate/invariant_finder.py | 2 +- src/translate/invariants.py | 6 ------ 2 files changed, 1 insertion(+), 7 deletions(-) diff --git a/src/translate/invariant_finder.py b/src/translate/invariant_finder.py index a4b01dcfeb..c88351d8ea 100755 --- a/src/translate/invariant_finder.py +++ b/src/translate/invariant_finder.py @@ -143,7 +143,7 @@ def useful_groups(invariants, initial_facts): # returns a list of mutex groups (parameters instantiated, counted variables not) def get_groups(task, reachable_action_params=None) -> List[List[pddl.Atom]]: with timers.timing("Finding invariants", block=True): - invariants = sorted(find_invariants(task, reachable_action_params)) + invariants = list(find_invariants(task, reachable_action_params)) with timers.timing("Checking invariant weight"): result = list(useful_groups(invariants, task.init)) return result diff --git a/src/translate/invariants.py b/src/translate/invariants.py index b5c30daaeb..9bd7bd4a6c 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -278,12 +278,6 @@ def __eq__(self, other): def __ne__(self, other): return self.parts != other.parts - def __lt__(self, other): - return self.parts < other.parts - - def __le__(self, other): - return self.parts <= other.parts - def __hash__(self): return hash(self.parts) From 9b2abd9b313d3c6b1681c0da9c849c414b8849c0 Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Tue, 6 Feb 2024 15:17:10 +0100 Subject: [PATCH 3/6] [issue879] (deterministically) randomize order in which invariant threats are considered --- src/translate/invariant_finder.py | 7 +++++++ src/translate/invariants.py | 16 +++++++++++++++- 2 files changed, 22 insertions(+), 1 deletion(-) diff --git a/src/translate/invariant_finder.py b/src/translate/invariant_finder.py index c88351d8ea..7d5ff039bf 100755 --- a/src/translate/invariant_finder.py +++ b/src/translate/invariant_finder.py @@ -3,6 +3,7 @@ from collections import deque, defaultdict import itertools +import random import time from typing import List @@ -104,6 +105,11 @@ def enqueue_func(invariant): candidates.append(invariant) seen_candidates.add(invariant) + # we want to fix the random seed for the invariant synthesis but don't want + # to have this a more global impact. For this reason, we temporary store + # the state of the random generator. + random_state = random.getstate() + random.seed(314159) start_time = time.process_time() while candidates: candidate = candidates.popleft() @@ -112,6 +118,7 @@ def enqueue_func(invariant): return if candidate.check_balance(balance_checker, enqueue_func): yield candidate + random.setstate(random_state) def useful_groups(invariants, initial_facts): predicate_to_invariants = defaultdict(list) diff --git a/src/translate/invariants.py b/src/translate/invariants.py index 9bd7bd4a6c..4aea69cc42 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -1,5 +1,6 @@ from collections import defaultdict import itertools +from random import randrange import constraints import pddl @@ -324,12 +325,25 @@ def check_balance(self, balance_checker, enqueue_func): # invariance analysis. for part in self.parts: actions_to_check.update(balance_checker.get_threats(part.predicate)) - for action in actions_to_check.keys(): + + # For a better expected perfomance, we want to randomize the order in + # which actions are checked. Since candidates are often already + # discarded by an early check, we do not want to shuffle the order but + # instead always draw the next action randomly from those we did not + # yet consider. + actions = list(actions_to_check.keys()) + unchecked = len(actions) + while unchecked: + pos = randrange(unchecked) + action = actions[pos] heavy_action = balance_checker.get_heavy_action(action) if self._operator_too_heavy(heavy_action): return False if self._operator_unbalanced(action, enqueue_func): return False + actions[pos], actions[unchecked - 1] = \ + actions[unchecked - 1], actions[pos] + unchecked -= 1 return True def _operator_too_heavy(self, h_action): From f6abb920b6b86a7fac8c2b246cd623e30a07adf0 Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Thu, 8 Feb 2024 08:34:33 +0100 Subject: [PATCH 4/6] [issue879] make parsing of initial state deterministic --- .../pddl_parser/parsing_functions.py | 36 +++++++++++-------- 1 file changed, 21 insertions(+), 15 deletions(-) diff --git a/src/translate/pddl_parser/parsing_functions.py b/src/translate/pddl_parser/parsing_functions.py index 33cbb00c4f..a0f263f400 100644 --- a/src/translate/pddl_parser/parsing_functions.py +++ b/src/translate/pddl_parser/parsing_functions.py @@ -573,8 +573,7 @@ def parse_axioms_and_actions(context, entries, type_dict, predicate_dict): def parse_init(context, alist): initial = [] - initial_true = set() - initial_false = set() + initial_proposition_values = dict() initial_assignments = dict() for no, fact in enumerate(alist[1:], start=1): with context.layer(f"Parsing {no}. element in init block"): @@ -611,15 +610,18 @@ def parse_init(context, alist): if not isinstance(fact, list) or not fact: context.error("Invalid negated fact.", syntax=SYNTAX_LITERAL_NEGATED) atom = pddl.Atom(fact[0], fact[1:]) - check_atom_consistency(context, atom, initial_false, initial_true, False) - initial_false.add(atom) + check_atom_consistency(context, atom, + initial_proposition_values, False) + initial_proposition_values[atom] = False else: if len(fact) < 1: context.error(f"Expecting {SYNTAX_LITERAL} for atoms.") atom = pddl.Atom(fact[0], fact[1:]) - check_atom_consistency(context, atom, initial_true, initial_false) - initial_true.add(atom) - initial.extend(initial_true) + check_atom_consistency(context, atom, + initial_proposition_values, True) + initial_proposition_values[atom] = True + initial.extend(atom for atom, val in initial_proposition_values.items() + if val is True) return initial @@ -802,14 +804,18 @@ def parse_task_pddl(context, task_pddl, type_dict, predicate_dict): assert False, "This line should be unreachable" -def check_atom_consistency(context, atom, same_truth_value, other_truth_value, atom_is_true=True): - if atom in other_truth_value: - context.error(f"Error in initial state specification\n" - f"Reason: {atom} is true and false.") - if atom in same_truth_value: - if not atom_is_true: - atom = atom.negate() - print(f"Warning: {atom} is specified twice in initial state specification") +def check_atom_consistency(context, atom, initial_proposition_values, + atom_value): + if atom in initial_proposition_values: + prev_value = initial_proposition_values[atom] + if prev_value != atom_value: + context.error(f"Error in initial state specification\n" + f"Reason: {atom} is true and false.") + else: + if atom_value is False: + atom = atom.negate() + print(f"Warning: {atom} is specified twice in initial state specification") + def check_for_duplicates(context, elements, errmsg, finalmsg): seen = set() From 9182878d40f861aeb8d58559632796bce4e0878e Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Thu, 8 Feb 2024 09:02:09 +0100 Subject: [PATCH 5/6] [issue879] remove other source of non-determinism; improve code --- src/translate/invariant_finder.py | 26 ++++++++++---------------- src/translate/invariants.py | 29 +++++++++++++---------------- 2 files changed, 23 insertions(+), 32 deletions(-) diff --git a/src/translate/invariant_finder.py b/src/translate/invariant_finder.py index 7d5ff039bf..9dded6dfab 100755 --- a/src/translate/invariant_finder.py +++ b/src/translate/invariant_finder.py @@ -14,11 +14,8 @@ class BalanceChecker: def __init__(self, task, reachable_action_params): - self.predicates_to_add_actions = defaultdict(dict) - # Conceptionally, predicates_to_add will store for each predicate the - # set of actions that have an add effect on the predicate. Since sets - # are not stable (introducing non-determinism in the algorithm), we - # store the actions as keys in a dictionary (which is stable). + self.predicates_to_add_actions = defaultdict(list) + self.random = random.Random(314159) self.action_to_heavy_action = {} for act in task.actions: action = self.add_inequality_preconds(act, reachable_action_params) @@ -32,7 +29,9 @@ def __init__(self, task, reachable_action_params): too_heavy_effects.append(eff.copy()) if not eff.literal.negated: predicate = eff.literal.predicate - self.predicates_to_add_actions[predicate][action] = True + add_actions = self.predicates_to_add_actions[predicate] + if not add_actions or add_actions[-1] is not action: + add_actions.append(action) if create_heavy_act: heavy_act = pddl.Action(action.name, action.parameters, action.num_external_parameters, @@ -43,7 +42,7 @@ def __init__(self, task, reachable_action_params): self.action_to_heavy_action[action] = heavy_act def get_threats(self, predicate): - return self.predicates_to_add_actions.get(predicate, dict()) + return self.predicates_to_add_actions.get(predicate, list()) def get_heavy_action(self, action): return self.action_to_heavy_action[action] @@ -105,11 +104,6 @@ def enqueue_func(invariant): candidates.append(invariant) seen_candidates.add(invariant) - # we want to fix the random seed for the invariant synthesis but don't want - # to have this a more global impact. For this reason, we temporary store - # the state of the random generator. - random_state = random.getstate() - random.seed(314159) start_time = time.process_time() while candidates: candidate = candidates.popleft() @@ -118,7 +112,6 @@ def enqueue_func(invariant): return if candidate.check_balance(balance_checker, enqueue_func): yield candidate - random.setstate(random_state) def useful_groups(invariants, initial_facts): predicate_to_invariants = defaultdict(list) @@ -126,7 +119,7 @@ def useful_groups(invariants, initial_facts): for predicate in invariant.predicates: predicate_to_invariants[predicate].append(invariant) - nonempty_groups = set() + nonempty_groups = dict() # dict instead of set because it is stable overcrowded_groups = set() for atom in initial_facts: if isinstance(atom, pddl.Assign): @@ -140,10 +133,11 @@ def useful_groups(invariants, initial_facts): group_key = (invariant, parameters_tuple) if group_key not in nonempty_groups: - nonempty_groups.add(group_key) + nonempty_groups[group_key] = True else: overcrowded_groups.add(group_key) - useful_groups = nonempty_groups - overcrowded_groups + useful_groups = [group_key for group_key in nonempty_groups.keys() + if group_key not in overcrowded_groups] for (invariant, parameters) in useful_groups: yield [part.instantiate(parameters) for part in sorted(invariant.parts)] diff --git a/src/translate/invariants.py b/src/translate/invariants.py index 4aea69cc42..a4d593a893 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -1,6 +1,5 @@ from collections import defaultdict import itertools -from random import randrange import constraints import pddl @@ -323,27 +322,25 @@ def check_balance(self, balance_checker, enqueue_func): # We will only use the keys of the dictionary. We do not use a set # because it's not stable and introduces non-determinism in the # invariance analysis. - for part in self.parts: - actions_to_check.update(balance_checker.get_threats(part.predicate)) - - # For a better expected perfomance, we want to randomize the order in - # which actions are checked. Since candidates are often already - # discarded by an early check, we do not want to shuffle the order but - # instead always draw the next action randomly from those we did not - # yet consider. + for part in sorted(self.parts): + for a in balance_checker.get_threats(part.predicate): + actions_to_check[a] = True + actions = list(actions_to_check.keys()) - unchecked = len(actions) - while unchecked: - pos = randrange(unchecked) - action = actions[pos] + while actions: + # For a better expected perfomance, we want to randomize the order + # in which actions are checked. Since candidates are often already + # discarded by an early check, we do not want to shuffle the order + # but instead always draw the next action randomly from those we + # did not yet consider. + pos = balance_checker.random.randrange(len(actions)) + actions[pos], actions[-1] = actions[-1], actions[pos] + action = actions.pop() heavy_action = balance_checker.get_heavy_action(action) if self._operator_too_heavy(heavy_action): return False if self._operator_unbalanced(action, enqueue_func): return False - actions[pos], actions[unchecked - 1] = \ - actions[unchecked - 1], actions[pos] - unchecked -= 1 return True def _operator_too_heavy(self, h_action): From b5977edda686791c9f995a96664fda455b403735 Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Thu, 8 Feb 2024 20:39:18 +0100 Subject: [PATCH 6/6] [issue879] remove unnecessary code --- src/translate/pddl_parser/parsing_functions.py | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/translate/pddl_parser/parsing_functions.py b/src/translate/pddl_parser/parsing_functions.py index a0f263f400..e21e81b9d3 100644 --- a/src/translate/pddl_parser/parsing_functions.py +++ b/src/translate/pddl_parser/parsing_functions.py @@ -614,8 +614,6 @@ def parse_init(context, alist): initial_proposition_values, False) initial_proposition_values[atom] = False else: - if len(fact) < 1: - context.error(f"Expecting {SYNTAX_LITERAL} for atoms.") atom = pddl.Atom(fact[0], fact[1:]) check_atom_consistency(context, atom, initial_proposition_values, True)