[issue879] make translator deterministic

On some domains such as citycar, repeated runs of the translator could
lead to different finite-domain encodings. In this issue we fixed several
sources of this non-deterministic behaviour.

src/translate/invariant_finder.py

@@ -3,6 +3,7 @@
 
 from collections import deque, defaultdict
 import itertools
+import random
 import time
 from typing import List
 
@@ -13,7 +14,8 @@
 
 class BalanceChecker:
     def __init__(self, task, reachable_action_params):
-        self.predicates_to_add_actions = defaultdict(set)
+        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)
@@ -27,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].add(action)
+                    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,
@@ -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, list())
 
     def get_heavy_action(self, action):
         return self.action_to_heavy_action[action]
@@ -115,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):
@@ -129,17 +133,18 @@ 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)]
 
 # 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

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)
 
@@ -324,10 +318,24 @@ def _get_cover_equivalence_conjunction(self, literal):
 
     def check_balance(self, balance_checker, enqueue_func):
         # Check balance for this hypothesis.
-        actions_to_check = set()
-        for part in self.parts:
-            actions_to_check |= balance_checker.get_threats(part.predicate)
-        for action in actions_to_check:
+        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 sorted(self.parts):
+            for a in balance_checker.get_threats(part.predicate):
+                actions_to_check[a] = True
+
+        actions = list(actions_to_check.keys())
+        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

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,16 @@ 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 +802,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()