From ff771eddd4a63aec25ab468d81f97c44d3748980 Mon Sep 17 00:00:00 2001 From: Marco Favorito Date: Sun, 9 Jul 2023 21:28:30 +0200 Subject: [PATCH 1/3] fix: use simplified mapping After this commit, there is no need to provide an explicit mapping, since it is assumed that the propositions *are* the ground fluents. E.g. if previously the formula was specified as follows: formula = "on_b_a & O(ontable_c)" Now we require that the propositions can be interpreted as PDDL predicates, i.e.: formula = '"on b a" & O("ontable c")' Pylogics does not allow spaces in the proposition name; therefore, the double quotes are always required. Only exception is when the predicate is unary: formula = 'Y(O(made-p4)))' (as in openstacks). --- README.md | 2 +- plan4past/__main__.py | 22 +-- plan4past/compiler.py | 38 +--- plan4past/helpers/utils.py | 52 +++-- plan4past/utils/derived_visitor.py | 62 ++---- plan4past/utils/mapping_parser.py | 186 ------------------ plan4past/utils/rewrite_formula_visitor.py | 4 + plan4past/utils/val_predicates_visitor.py | 2 +- .../BF/elevators_ppltl/elevators_teg.json | 58 +++--- tests/test_compiler/test_blocksworld_det.py | 2 +- tests/test_compiler/test_readme_example.py | 21 +- tests/test_helpers/test_utils.py | 22 --- tests/test_utils/test_derived_visitor.py | 45 ++--- tests/test_utils/test_mapping_parser.py | 168 ---------------- .../test_rewrite_formula_visitor.py | 44 ++--- 15 files changed, 144 insertions(+), 584 deletions(-) delete mode 100644 plan4past/utils/mapping_parser.py delete mode 100644 tests/test_utils/test_mapping_parser.py diff --git a/README.md b/README.md index 417f8e88..d9ebef52 100644 --- a/README.md +++ b/README.md @@ -41,7 +41,7 @@ from pddl.parser.problem import ProblemParser from pylogics.parsers import parse_pltl from plan4past.compiler import Compiler -formula = "on_b_a & O(ontable_c)" +formula = '"on b a" & O("ontable c")' domain_parser = DomainParser() problem_parser = ProblemParser() diff --git a/plan4past/__main__.py b/plan4past/__main__.py index 543603c0..c7c12c9c 100644 --- a/plan4past/__main__.py +++ b/plan4past/__main__.py @@ -34,7 +34,6 @@ from pylogics.syntax.base import Formula from plan4past.compiler import Compiler -from plan4past.utils.mapping_parser import mapping_parser DEFAULT_NEW_DOMAIN_FILENAME: str = "new-domain.pddl" DEFAULT_NEW_PROBLEM_FILENAME: str = "new-problem.pddl" @@ -62,13 +61,6 @@ help="The path to the PPLTL goal formula.", type=click.Path(exists=True, readable=True), ) -@click.option( - "-m", - "--mapping", - help="The mapping file.", - type=click.Path(exists=True, readable=True), - default=None, -) @click.option( "-od", "--out-domain", @@ -83,20 +75,14 @@ help="Path to PDDL file to store the new problem.", type=click.Path(dir_okay=False), ) -def cli(domain, problem, goal_inline, goal_file, mapping, out_domain, out_problem): +def cli(domain, problem, goal_inline, goal_file, out_domain, out_problem): """Plan4Past: Planning for Pure-Past Temporally Extended Goals.""" goal = _get_goal(goal_inline, goal_file) in_domain, in_problem, formula = _parse_instance(domain, problem, goal) - var_map = ( - mapping_parser(Path(mapping).read_text(encoding="utf-8"), formula) - if mapping - else None - ) - compiled_domain, compiled_problem = _compile_instance( - in_domain, in_problem, formula, var_map + in_domain, in_problem, formula ) try: @@ -137,9 +123,9 @@ def _parse_instance(in_domain, in_problem, goal) -> Tuple[Domain, Problem, Formu return domain, problem, formula -def _compile_instance(domain, problem, formula, mapping) -> Tuple[Domain, Problem]: +def _compile_instance(domain, problem, formula) -> Tuple[Domain, Problem]: """Compile the PDDL domain and problem files and the PPLTL goal formula.""" - compiler = Compiler(domain, problem, formula, mapping) + compiler = Compiler(domain, problem, formula) compiler.compile() compiled_domain, compiled_problem = compiler.result diff --git a/plan4past/compiler.py b/plan4past/compiler.py index 6fec28b4..cb9478ba 100644 --- a/plan4past/compiler.py +++ b/plan4past/compiler.py @@ -21,10 +21,9 @@ # """Compiler from PDDL Domain and PPLTL into a new PDDL domain.""" -from typing import AbstractSet, Dict, Optional, Set, Tuple +from typing import AbstractSet, Optional, Set, Tuple from pddl.core import Action, Domain, Problem, Requirements -from pddl.logic import Constant from pddl.logic.base import And, Not from pddl.logic.effects import AndEffect, When from pddl.logic.predicates import DerivedPredicate, Predicate @@ -35,7 +34,6 @@ from plan4past.helpers.utils import ( add_val_prefix, check_, - default_mapping, remove_before_prefix, replace_symbols, ) @@ -54,7 +52,6 @@ def __init__( domain: Domain, problem: Problem, formula: Formula, - from_atoms_to_fluent: Optional[Dict[PLTLAtomic, Predicate]] = None, ) -> None: """ Initialize the compiler. @@ -62,16 +59,10 @@ def __init__( :param domain: the domain :param problem: the problem :param formula: the formula - :param from_atoms_to_fluent: optional mapping from atoms to fluent """ self.domain = domain self.problem = problem self.formula = rewrite(formula) - if from_atoms_to_fluent: - self.from_atoms_to_fluent = from_atoms_to_fluent - self.validate_mapping(domain, formula, from_atoms_to_fluent) - else: - self.from_atoms_to_fluent = default_mapping(self.formula) check_(self.formula.logic == Logic.PLTL, "only PPLTL is supported!") @@ -81,29 +72,6 @@ def __init__( self._derived_predicates: Set[DerivedPredicate] = set() - @classmethod - def validate_mapping( - cls, - _domain: Domain, - _formula: Formula, - from_atoms_to_fluent: Dict[PLTLAtomic, Predicate], - ): - """ - Check that the mapping is valid wrt the problem instance. - - In particular: - - check that all the formula atoms are covered (TODO) - - check that all the atoms are legal wrt the formula - - check that the fluents are legal wrt the domain - - :param _domain: - :param _formula: - :param from_atoms_to_fluent: - :return: - """ - for _atom, fluent in from_atoms_to_fluent.items(): - check_(all(isinstance(t, Constant) for t in fluent.terms)) - @property def result(self) -> Tuple[Domain, Problem]: """Get the result.""" @@ -121,9 +89,7 @@ def compile(self): def _compile_domain(self): """Compute the new domain.""" new_predicates = predicates(self.formula).union(val_predicates(self.formula)) - new_derived_predicates = derived_predicates( - self.formula, self.from_atoms_to_fluent - ) + new_derived_predicates = derived_predicates(self.formula) new_whens = _compute_whens(self.formula) domain_actions = _update_domain_actions_det(self.domain.actions, new_whens) diff --git a/plan4past/helpers/utils.py b/plan4past/helpers/utils.py index a1b47738..3175f59f 100644 --- a/plan4past/helpers/utils.py +++ b/plan4past/helpers/utils.py @@ -21,13 +21,14 @@ # """Miscellanea utilities.""" -from typing import Dict +import re from pddl.logic import Predicate, constants -from pylogics.syntax.base import Formula -from pylogics.syntax.pltl import Atomic as PLTLAtomic -from plan4past.utils.atoms_visitor import find_atoms +_PDDL_NAME_REGEX = "[A-Za-z][-_A-Za-z0-9]*" +_GROUND_FLUENT_REGEX = re.compile( + rf"(\"({_PDDL_NAME_REGEX})( {_PDDL_NAME_REGEX})*\")|({_PDDL_NAME_REGEX})" +) def add_val_prefix(name: str): @@ -65,19 +66,6 @@ def replace_symbols(name: str): ) -def default_mapping(formula: Formula) -> Dict[PLTLAtomic, Predicate]: - """Compute mapping from atoms to fluents using underscores.""" - symbols = find_atoms(formula) - from_atoms_to_fluents = {} - for symbol in symbols: - name, *cons = symbol.name.split("_") - if cons: - from_atoms_to_fluents[symbol] = Predicate(name, *constants(" ".join(cons))) - else: - from_atoms_to_fluents[symbol] = Predicate(name) - return from_atoms_to_fluents - - def check_(condition: bool, message: str = "") -> None: """ User-defined assert. @@ -88,3 +76,33 @@ def check_(condition: bool, message: str = "") -> None: """ if not condition: raise AssertionError(message) + + +def parse_ground_fluent(symbol: str) -> Predicate: + """ + Parse a ground fluent. + + :param symbol: the ground fluent + :return: the predicate + """ + match = _GROUND_FLUENT_REGEX.fullmatch(symbol) + if match is None: + raise ValueError(f"invalid PDDL symbol in formula: {symbol}") + + if '"' in symbol: + tokens = symbol[1:-1].split(" ", 1) + predicate_name, cons = ( + (tokens[0], tokens[1]) if len(tokens) > 1 else (tokens[0], "") + ) + return Predicate(predicate_name, *constants(cons)) + return Predicate(symbol) + + +def validate(symbol: str) -> None: + """ + Validate a symbol. + + :param symbol: the symbol + """ + # check if the symbol is a valid PDDL ground fluent + parse_ground_fluent(symbol) diff --git a/plan4past/utils/derived_visitor.py b/plan4past/utils/derived_visitor.py index 7988d326..e0be5143 100644 --- a/plan4past/utils/derived_visitor.py +++ b/plan4past/utils/derived_visitor.py @@ -22,7 +22,7 @@ """Derived Predicates visitor.""" from functools import singledispatch -from typing import Dict, Set +from typing import Set from pddl.logic.base import And, Not, Or from pddl.logic.predicates import DerivedPredicate, Predicate @@ -39,49 +39,39 @@ ) from pylogics.utils.to_string import to_string -from plan4past.helpers.utils import add_val_prefix, replace_symbols +from plan4past.helpers.utils import add_val_prefix, parse_ground_fluent, replace_symbols @singledispatch -def derived_predicates( - formula: object, atoms_to_fluents: Dict[PLTLAtomic, Predicate] -) -> Set[DerivedPredicate]: +def derived_predicates(formula: object) -> Set[DerivedPredicate]: """Compute the derived predicate for a formula.""" raise NotImplementedError(f"handler not implemented for object {type(formula)}") @derived_predicates.register -def derived_predicates_true( - _formula: PropositionalTrue, _atoms_to_fluents: Dict[PLTLAtomic, Predicate] -) -> Set[DerivedPredicate]: +def derived_predicates_true(_formula: PropositionalTrue) -> Set[DerivedPredicate]: """Compute the derived predicate for a true formula.""" val = Predicate(add_val_prefix("true")) return {DerivedPredicate(val, And())} @derived_predicates.register -def derived_predicates_false( - _formula: PropositionalFalse, _atoms_to_fluents: Dict[PLTLAtomic, Predicate] -) -> Set[DerivedPredicate]: +def derived_predicates_false(_formula: PropositionalFalse) -> Set[DerivedPredicate]: """Compute the derived predicate for a false formula.""" val = Predicate(add_val_prefix("false")) return {DerivedPredicate(val, Or())} @derived_predicates.register -def derived_predicates_atomic( - formula: PLTLAtomic, atoms_to_fluents: Dict[PLTLAtomic, Predicate] -) -> Set[DerivedPredicate]: +def derived_predicates_atomic(formula: PLTLAtomic) -> Set[DerivedPredicate]: """Compute the derived predicate for an atomic formula.""" - val = Predicate(add_val_prefix(formula.name)) - condition = atoms_to_fluents[formula] + val = Predicate(add_val_prefix(replace_symbols(formula.name))) + condition = parse_ground_fluent(formula.name) return {DerivedPredicate(val, condition)} @derived_predicates.register -def derived_predicates_and( - formula: PLTLAnd, atoms_to_fluents: Dict[PLTLAtomic, Predicate] -) -> Set[DerivedPredicate]: +def derived_predicates_and(formula: PLTLAnd) -> Set[DerivedPredicate]: """Compute the derived predicate for a PPLTL And formula.""" formula_name = to_string(formula) val = Predicate(add_val_prefix(replace_symbols(formula_name))) @@ -90,14 +80,12 @@ def derived_predicates_and( for op in formula.operands ] condition = And(*val_ops) - der_pred_ops = [derived_predicates(op, atoms_to_fluents) for op in formula.operands] + der_pred_ops = [derived_predicates(op) for op in formula.operands] return {DerivedPredicate(val, condition)}.union(*der_pred_ops) @derived_predicates.register -def derived_predicates_or( - formula: PLTLOr, atoms_to_fluents: Dict[PLTLAtomic, Predicate] -) -> Set[DerivedPredicate]: +def derived_predicates_or(formula: PLTLOr) -> Set[DerivedPredicate]: """Compute the derived predicate for a PPLTL Or formula.""" formula_name = to_string(formula) val = Predicate(add_val_prefix(replace_symbols(formula_name))) @@ -106,45 +94,39 @@ def derived_predicates_or( for op in formula.operands ] condition = Or(*val_ops) - der_pred_ops = [derived_predicates(op, atoms_to_fluents) for op in formula.operands] + der_pred_ops = [derived_predicates(op) for op in formula.operands] return {DerivedPredicate(val, condition)}.union(*der_pred_ops) @derived_predicates.register -def derived_predicates_not( - formula: PLTLNot, atoms_to_fluents: Dict[PLTLAtomic, Predicate] -) -> Set[DerivedPredicate]: +def derived_predicates_not(formula: PLTLNot) -> Set[DerivedPredicate]: """Compute the derived predicate for a PPLTL Not formula.""" formula_name = to_string(formula) val = Predicate(add_val_prefix(replace_symbols(formula_name))) condition = Not( Predicate(add_val_prefix(replace_symbols(to_string(formula.argument)))) ) - der_pred_arg = derived_predicates(formula.argument, atoms_to_fluents) + der_pred_arg = derived_predicates(formula.argument) return {DerivedPredicate(val, condition)}.union(der_pred_arg) @derived_predicates.register -def derived_predicates_before( - formula: Before, atoms_to_fluents: Dict[PLTLAtomic, Predicate] -) -> Set[DerivedPredicate]: +def derived_predicates_before(formula: Before) -> Set[DerivedPredicate]: """Compute the derived predicate for a Before formula.""" formula_name = to_string(formula) val = Predicate(add_val_prefix(replace_symbols(formula_name))) condition = Predicate(replace_symbols(to_string(formula))) - der_pred_arg = derived_predicates(formula.argument, atoms_to_fluents) + der_pred_arg = derived_predicates(formula.argument) return {DerivedPredicate(val, condition)}.union(der_pred_arg) @derived_predicates.register -def derived_predicates_since( - formula: Since, atoms_to_fluents: Dict[PLTLAtomic, Predicate] -) -> Set[DerivedPredicate]: +def derived_predicates_since(formula: Since) -> Set[DerivedPredicate]: """Compute the derived predicate for a Since formula.""" if len(formula.operands) != 2: head = formula.operands[0] tail = Since(*formula.operands[1:]) - return derived_predicates(Since(head, tail), atoms_to_fluents) + return derived_predicates(Since(head, tail)) formula_name = to_string(formula) val = Predicate(add_val_prefix(replace_symbols(formula_name))) op_or_1 = Predicate(add_val_prefix(replace_symbols(to_string(formula.operands[1])))) @@ -153,14 +135,12 @@ def derived_predicates_since( Predicate(f"Y-{replace_symbols(to_string(formula))}"), ) condition = Or(op_or_1, op_or_2) - der_pred_ops = [derived_predicates(op, atoms_to_fluents) for op in formula.operands] + der_pred_ops = [derived_predicates(op) for op in formula.operands] return {DerivedPredicate(val, condition)}.union(*der_pred_ops) @derived_predicates.register -def derived_predicates_once( - formula: Once, atoms_to_fluents: Dict[PLTLAtomic, Predicate] -) -> Set[DerivedPredicate]: +def derived_predicates_once(formula: Once) -> Set[DerivedPredicate]: """Compute the derived predicate for a Once formula.""" formula_name = to_string(formula) val = Predicate(add_val_prefix(replace_symbols(formula_name))) @@ -168,5 +148,5 @@ def derived_predicates_once( Predicate(add_val_prefix(replace_symbols(to_string(formula.argument)))), Predicate(f"Y-{replace_symbols(to_string(formula))}"), ) - der_pred_arg = derived_predicates(formula.argument, atoms_to_fluents) + der_pred_arg = derived_predicates(formula.argument) return {DerivedPredicate(val, condition)}.union(der_pred_arg) diff --git a/plan4past/utils/mapping_parser.py b/plan4past/utils/mapping_parser.py deleted file mode 100644 index f1e9f177..00000000 --- a/plan4past/utils/mapping_parser.py +++ /dev/null @@ -1,186 +0,0 @@ -# -*- coding: utf-8 -*- -# -# Copyright 2021 -- 2023 WhiteMech -# -# ------------------------------ -# -# This file is part of Plan4Past. -# -# Plan4Past is free software: you can redistribute it and/or modify -# it under the terms of the GNU Lesser General Public License as published by -# the Free Software Foundation, either version 3 of the License, or -# (at your option) any later version. -# -# Plan4Past is distributed in the hope that it will be useful, -# but WITHOUT ANY WARRANTY; without even the implied warranty of -# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -# GNU Lesser General Public License for more details. -# -# You should have received a copy of the GNU Lesser General Public License -# along with Plan4Past. If not, see . -# - -"""Mapping parser.""" -import re -from typing import Dict, Optional, Sequence, Set, Tuple - -from pddl.custom_types import name -from pddl.logic import Constant, Predicate, constants -from pylogics.syntax.base import Formula -from pylogics.syntax.pltl import Atomic as PLTLAtomic - -from plan4past.utils.atoms_visitor import find_atoms - - -class MappingParserError(Exception): - """Mapping parser error.""" - - def __init__(self, message: str, *args, row_id: Optional[int] = None) -> None: - """ - Initialize a mapping parser error. - - :param row_id: the row id - """ - self.row_id = row_id - - super().__init__(self._make_message_prefix() + message, *args) - - def _make_message_prefix(self) -> str: - """Make the message prefix.""" - if self.row_id is None: - return "invalid mapping: " - return f"invalid mapping at row {self.row_id}: " - - -SYMBOL_REGEX = re.compile("[a-z_]([a-zA-Z0-9_-]+[a-zA-Z0-9_])|[a-z_][a-zA-Z0-9_]*") -"""The following is a sub-regex of AtomName.REGEX in pylogics.syntax.base.""" - - -def _check_pddl_name(row_id: int, pddl_name: str, what: str) -> None: - """Check that a PDDL name is valid.""" - try: - name(pddl_name) - except ValueError as e: - raise MappingParserError( - f"got an invalid name for {what}: '{pddl_name}'. It must match the regex {name.REGEX}", - row_id=row_id, - ) from e - - -def _parse_constants(row_id: int, constants_str: str) -> Sequence[Constant]: - """ - Parse a string of constants. - - :param row_id: the row id - :param constants_str: the string of constants - :return: the sequence of constants - """ - try: - return constants(constants_str) - except ValueError as e: - raise MappingParserError(f"got an invalid constant: {e}", row_id=row_id) from e - - -def _parse_predicate(row_id: int, predicate_str: str) -> Predicate: - """ - Parse a predicate. - - :param predicate_str: the predicate string - :return: the predicate - """ - predicate_name, cons = predicate_str.split(" ", maxsplit=1) - - _check_pddl_name(row_id, predicate_name, "a predicate") - parsed_constants = _parse_constants(row_id, cons) - return Predicate(predicate_name, *parsed_constants) - - -def _process_row(row_id: int, row_str: str) -> Tuple[str, Predicate]: - """ - Process a row of the mapping file. - - :param row_id: the row id - :param row_str: the row string - :return: the pair (symbol_name, predicate_str) - """ - # check the row is a valid mapping - comma_separated_row_parts = row_str.split(",") - if len(comma_separated_row_parts) != 2: - raise MappingParserError( - "expected a mapping of the form ','", row_id=row_id - ) - - symbol_name, predicate = comma_separated_row_parts - - # strip leading and trailing whitespaces - symbol_name = symbol_name.strip() - predicate_str = predicate.strip() - - if symbol_name == "" or SYMBOL_REGEX.fullmatch(symbol_name) is None: - raise MappingParserError( - "symbol cannot be empty string and must match the regex {SYMBOL_REGEX}", - row_id=row_id, - ) - if predicate_str == "": - raise MappingParserError("predicate cannot be empty string", row_id=row_id) - - predicate = _parse_predicate(row_id, predicate_str) - return symbol_name, predicate - - -def _check_unmapped_symbols( - all_symbol_names: Set[str], mapped_symbol_names: Set[str] -) -> None: - """Check that all symbols are mapped.""" - # check if there are unmapped symbols (exclude 'true' and 'false') - unmapped_symbols = all_symbol_names - {"true", "false"} - mapped_symbol_names - # if some symbols are not mapped, raise an error - if unmapped_symbols: - raise MappingParserError( - f"the following symbols of the formula are not mapped: {unmapped_symbols}" - ) - - -def should_skip_row(row_str: str) -> bool: - """Check if a row should be skipped.""" - # skip empty lines - if row_str.strip() == "": - return True - - # skip comments - if row_str.strip().startswith(";"): - return True - - return False - - -def mapping_parser(text: str, formula: Formula) -> Dict[PLTLAtomic, Predicate]: - """Parse symbols to ground predicates mapping.""" - symbols = find_atoms(formula) - symbols_by_name = {symbol.name: symbol for symbol in symbols} - maps = text.splitlines(keepends=False) - from_atoms_to_fluents = {} - mapped_symbol_names = set() - - for row_id, vmap in enumerate(maps): - if should_skip_row(vmap): - continue - - symbol_name, predicate = _process_row(row_id, vmap) - - if symbol_name not in symbols_by_name: - # don't need to process this row, since the symbol does not occur in the formula - continue - - if symbol_name in mapped_symbol_names: - raise MappingParserError( - f"symbol '{symbol_name}' is mapped multiple times", row_id=row_id - ) - - symbol = symbols_by_name[symbol_name] - mapped_symbol_names.add(symbol_name) - - from_atoms_to_fluents[symbol] = predicate - - _check_unmapped_symbols(set(symbols_by_name.keys()), mapped_symbol_names) - return from_atoms_to_fluents diff --git a/plan4past/utils/rewrite_formula_visitor.py b/plan4past/utils/rewrite_formula_visitor.py index d0981895..36162b9a 100644 --- a/plan4past/utils/rewrite_formula_visitor.py +++ b/plan4past/utils/rewrite_formula_visitor.py @@ -40,6 +40,8 @@ Since, ) +from plan4past.helpers.utils import validate + def rewrite_unaryop(formula: _UnaryOp): """Rewrite the formula for a unary operator.""" @@ -69,6 +71,8 @@ def rewrite_false(formula: PropositionalFalse) -> Formula: @rewrite.register def rewrite_atomic(formula: PLTLAtomic) -> Formula: """Compute the basic formula for an atomic formula.""" + # validate atomic formula symbol - it must be a PDDL ground fluent + validate(formula.name) return formula diff --git a/plan4past/utils/val_predicates_visitor.py b/plan4past/utils/val_predicates_visitor.py index 83ae37b0..a1c7006e 100644 --- a/plan4past/utils/val_predicates_visitor.py +++ b/plan4past/utils/val_predicates_visitor.py @@ -76,7 +76,7 @@ def val_predicates_false(_formula: PropositionalFalse) -> Set[Predicate]: @val_predicates.register def val_predicates_atomic(formula: PLTLAtomic) -> Set[Predicate]: """Compute the value predicate for an atomic formula.""" - return {Predicate(add_val_prefix(formula.name))} + return {Predicate(add_val_prefix(replace_symbols(formula.name)))} @val_predicates.register diff --git a/tests/benchmarks/deterministic/BF/elevators_ppltl/elevators_teg.json b/tests/benchmarks/deterministic/BF/elevators_ppltl/elevators_teg.json index c062b3c8..70b5d880 100644 --- a/tests/benchmarks/deterministic/BF/elevators_ppltl/elevators_teg.json +++ b/tests/benchmarks/deterministic/BF/elevators_ppltl/elevators_teg.json @@ -1,31 +1,31 @@ { - "s2-0": "O(served_p1) & O(served_p0 & !(Y(O(served_p1))))", - "s3-0": "O(served_p1 & served_p2) & O(served_p0 & !(Y(O(served_p1 | served_p2)))) & !(O(boarded_p0 & boarded_p1)) & !(O(boarded_p1 & boarded_p2)) & !(O(boarded_p2 & boarded_p0))", - "s4-0": "O(served_p2 & served_p3) & O(served_p0 & served_p1 & !(Y(O(served_p2 | served_p3)))) & !(O(boarded_p0 & boarded_p1)) & !(O(boarded_p1 & boarded_p2)) & !(O(boarded_p2 & boarded_p3)) & !(O(boarded_p3 & boarded_p0))", - "s5-0": "O(served_p2 & served_p3 & served_p4) & O(served_p0 & served_p1 & !(Y(O(served_p2 | served_p3 | served_p4)))) & !(O(boarded_p0 & boarded_p1)) & !(O(boarded_p1 & boarded_p2)) & !(O(boarded_p2 & boarded_p3)) & !(O(boarded_p3 & boarded_p4)) & !(O(boarded_p4 & boarded_p0))", - "s6-0": "O(served_p3 & served_p4 & served_p5) & O(served_p0 & served_p1 & served_p2 & !(Y(O(served_p3 | served_p4 | served_p5)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5))) & !(O(boarded_p4 & (boarded_p5 | boarded_p0))) & !(O(boarded_p5 & (boarded_p0 | boarded_p1)))", - "s7-0": "O(served_p3 & served_p4 & served_p5 & served_p6) & O(served_p0 & served_p1 & served_p2 & !(Y(O(served_p3 | served_p4 | served_p5 | served_p6)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6))) & !(O(boarded_p5 & (boarded_p6 | boarded_p0))) & !(O(boarded_p6 & (boarded_p0 | boarded_p1)))", - "s8-0": "O(served_p4 & served_p5 & served_p6 & served_p7) & O(served_p0 & served_p1 & served_p2 & served_p3 & !(Y(O(served_p4 | served_p5 | served_p6 | served_p7)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7))) & !(O(boarded_p6 & (boarded_p7 | boarded_p0))) & !(O(boarded_p7 & (boarded_p0 | boarded_p1)))", - "s9-0": "O(served_p4 & served_p5 & served_p6 & served_p7 & served_p8) & O(served_p0 & served_p1 & served_p2 & served_p3 & !(Y(O(served_p4 | served_p5 | served_p6 | served_p7 | served_p8)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p0))) & !(O(boarded_p7 & (boarded_p8 | boarded_p0 | boarded_p1))) & !(O(boarded_p8 & (boarded_p0 | boarded_p1 | boarded_p2)))", - "s10-0": "O(served_p5 & served_p6 & served_p7 & served_p8 & served_p9) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & !(Y(O(served_p5 | served_p6 | served_p7 | served_p8 | served_p9)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p0))) & !(O(boarded_p8 & (boarded_p9 | boarded_p0 | boarded_p1))) & !(O(boarded_p9 & (boarded_p0 | boarded_p1 | boarded_p2)))", - "s11-0": "O(served_p5 & served_p6 & served_p7 & served_p8 & served_p9 & served_p10) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & !(Y(O(served_p5 | served_p6 | served_p7 | served_p8 | served_p9 | served_p10)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p0))) & !(O(boarded_p9 & (boarded_p10 | boarded_p0 | boarded_p1))) & !(O(boarded_p10 & (boarded_p0 | boarded_p1 | boarded_p2)))", - "s12-0": "O(served_p6 & served_p7 & served_p8 & served_p9 & served_p10 & served_p11) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & !(Y(O(served_p6 | served_p7 | served_p8 | served_p9 | served_p10 | served_p11)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p0))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p0 | boarded_p1))) & !(O(boarded_p10 & (boarded_p11 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p11 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3)))", - "s13-0": "O(served_p6 & served_p7 & served_p8 & served_p9 & served_p10 & served_p11 & served_p12) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & !(Y(O(served_p6 | served_p7 | served_p8 | served_p9 | served_p10 | served_p11 | served_p12)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p0))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p0 | boarded_p1))) & !(O(boarded_p11 & (boarded_p12 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p12 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3)))", - "s14-0": "O(served_p7 & served_p8 & served_p9 & served_p10 & served_p11 & served_p12 & served_p13) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & !(Y(O(served_p7 | served_p8 | served_p9 | served_p10 | served_p11 | served_p12 | served_p13)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p0))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p0 | boarded_p1))) & !(O(boarded_p12 & (boarded_p13 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p13 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3)))", - "s15-0": "O(served_p7 & served_p8 & served_p9 & served_p10 & served_p11 & served_p12 & served_p13 & served_p14) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & !(Y(O(served_p7 | served_p8 | served_p9 | served_p10 | served_p11 | served_p12 | served_p13 | served_p14)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p0))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p0 | boarded_p1))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p13 & (boarded_p14 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p14 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4)))", - "s16-0": "O(served_p8 & served_p9 & served_p10 & served_p11 & served_p12 & served_p13 & served_p14 & served_p15) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & !(Y(O(served_p8 | served_p9 | served_p10 | served_p11 | served_p12 | served_p13 | served_p14 | served_p15)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p0))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p0 | boarded_p1))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p14 & (boarded_p15 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p15 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4)))", - "s17-0": "O(served_p8 & served_p9 & served_p10 & served_p11 & served_p12 & served_p13 & served_p14 & served_p15 & served_p16) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & !(Y(O(served_p8 | served_p9 | served_p10 | served_p11 | served_p12 | served_p13 | served_p14 | served_p15 | served_p16)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p0))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p0 | boarded_p1))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p15 & (boarded_p16 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p16 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4)))", - "s18-0": "O(served_p9 & served_p10 & served_p11 & served_p12 & served_p13 & served_p14 & served_p15 & served_p16 & served_p17) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & served_p8 & !(Y(O(served_p9 | served_p10 | served_p11 | served_p12 | served_p13 | served_p14 | served_p15 | served_p16 | served_p17)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p0))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p0 | boarded_p1))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p17 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p15 & (boarded_p16 | boarded_p17 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p16 & (boarded_p17 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p17 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5)))", - "s19-0": "O(served_p9 & served_p10 & served_p11 & served_p12 & served_p13 & served_p14 & served_p15 & served_p16 & served_p17 & served_p18) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & served_p8 & !(Y(O(served_p9 | served_p10 | served_p11 | served_p12 | served_p13 | served_p14 | served_p15 | served_p16 | served_p17 | served_p18)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p0))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p0 | boarded_p1))) & !(O(boarded_p15 & (boarded_p16 | boarded_p17 | boarded_p18 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p16 & (boarded_p17 | boarded_p18 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p17 & (boarded_p18 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p18 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5)))", - "s20-0": "O(served_p10 & served_p11 & served_p12 & served_p13 & served_p14 & served_p15 & served_p16 & served_p17 & served_p18 & served_p19) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & served_p8 & served_p9 & !(Y(O(served_p10 | served_p11 | served_p12 | served_p13 | served_p14 | served_p15 | served_p16 | served_p17 | served_p18 | served_p19)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p0))) & !(O(boarded_p15 & (boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p0 | boarded_p1))) & !(O(boarded_p16 & (boarded_p17 | boarded_p18 | boarded_p19 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p17 & (boarded_p18 | boarded_p19 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p18 & (boarded_p19 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p19 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5)))", - "s21-0": "O(served_p10 & served_p11 & served_p12 & served_p13 & served_p14 & served_p15 & served_p16 & served_p17 & served_p18 & served_p19 & served_p20) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & served_p8 & served_p9 & !(Y(O(served_p10 | served_p11 | served_p12 | served_p13 | served_p14 | served_p15 | served_p16 | served_p17 | served_p18 | served_p19 | served_p20)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p0))) & !(O(boarded_p15 & (boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p0 | boarded_p1))) & !(O(boarded_p16 & (boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p17 & (boarded_p18 | boarded_p19 | boarded_p20 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p18 & (boarded_p19 | boarded_p20 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p19 & (boarded_p20 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p20 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6)))", - "s22-0": "O(served_p11 & served_p12 & served_p13 & served_p14 & served_p15 & served_p16 & served_p17 & served_p18 & served_p19 & served_p20 & served_p21) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & served_p8 & served_p9 & served_p10 & !(Y(O(served_p11 | served_p12 | served_p13 | served_p14 | served_p15 | served_p16 | served_p17 | served_p18 | served_p19 | served_p20 | served_p21)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21))) & !(O(boarded_p15 & (boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p0))) & !(O(boarded_p16 & (boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p0 | boarded_p1))) & !(O(boarded_p17 & (boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p18 & (boarded_p19 | boarded_p20 | boarded_p21 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p19 & (boarded_p20 | boarded_p21 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p20 & (boarded_p21 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p21 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6)))", - "s23-0": "O(served_p11 & served_p12 & served_p13 & served_p14 & served_p15 & served_p16 & served_p17 & served_p18 & served_p19 & served_p20 & served_p21 & served_p22) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & served_p8 & served_p9 & served_p10 & !(Y(O(served_p11 | served_p12 | served_p13 | served_p14 | served_p15 | served_p16 | served_p17 | served_p18 | served_p19 | served_p20 | served_p21 | served_p22)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21))) & !(O(boarded_p15 & (boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22))) & !(O(boarded_p16 & (boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p0))) & !(O(boarded_p17 & (boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p0 | boarded_p1))) & !(O(boarded_p18 & (boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p19 & (boarded_p20 | boarded_p21 | boarded_p22 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p20 & (boarded_p21 | boarded_p22 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p21 & (boarded_p22 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p22 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6)))", - "s24-0": "O(served_p12 & served_p13 & served_p14 & served_p15 & served_p16 & served_p17 & served_p18 & served_p19 & served_p20 & served_p21 & served_p22 & served_p23) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & served_p8 & served_p9 & served_p10 & served_p11 & !(Y(O(served_p12 | served_p13 | served_p14 | served_p15 | served_p16 | served_p17 | served_p18 | served_p19 | served_p20 | served_p21 | served_p22 | served_p23)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22))) & !(O(boarded_p15 & (boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23))) & !(O(boarded_p16 & (boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p0))) & !(O(boarded_p17 & (boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p0 | boarded_p1))) & !(O(boarded_p18 & (boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p19 & (boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p20 & (boarded_p21 | boarded_p22 | boarded_p23 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p21 & (boarded_p22 | boarded_p23 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p22 & (boarded_p23 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p23 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7)))", - "s25-0": "O(served_p12 & served_p13 & served_p14 & served_p15 & served_p16 & served_p17 & served_p18 & served_p19 & served_p20 & served_p21 & served_p22 & served_p23 & served_p24) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & served_p8 & served_p9 & served_p10 & served_p11 & !(Y(O(served_p12 | served_p13 | served_p14 | served_p15 | served_p16 | served_p17 | served_p18 | served_p19 | served_p20 | served_p21 | served_p22 | served_p23 | served_p24)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22))) & !(O(boarded_p15 & (boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23))) & !(O(boarded_p16 & (boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24))) & !(O(boarded_p17 & (boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p0))) & !(O(boarded_p18 & (boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p0 | boarded_p1))) & !(O(boarded_p19 & (boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p20 & (boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p21 & (boarded_p22 | boarded_p23 | boarded_p24 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p22 & (boarded_p23 | boarded_p24 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p23 & (boarded_p24 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p24 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7)))", - "s26-0": "O(served_p13 & served_p14 & served_p15 & served_p16 & served_p17 & served_p18 & served_p19 & served_p20 & served_p21 & served_p22 & served_p23 & served_p24 & served_p25) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & served_p8 & served_p9 & served_p10 & served_p11 & served_p12 & !(Y(O(served_p13 | served_p14 | served_p15 | served_p16 | served_p17 | served_p18 | served_p19 | served_p20 | served_p21 | served_p22 | served_p23 | served_p24 | served_p25)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22))) & !(O(boarded_p15 & (boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23))) & !(O(boarded_p16 & (boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24))) & !(O(boarded_p17 & (boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25))) & !(O(boarded_p18 & (boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p0))) & !(O(boarded_p19 & (boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p0 | boarded_p1))) & !(O(boarded_p20 & (boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p21 & (boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p22 & (boarded_p23 | boarded_p24 | boarded_p25 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p23 & (boarded_p24 | boarded_p25 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p24 & (boarded_p25 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p25 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7)))", - "s27-0": "O(served_p13 & served_p14 & served_p15 & served_p16 & served_p17 & served_p18 & served_p19 & served_p20 & served_p21 & served_p22 & served_p23 & served_p24 & served_p25 & served_p26) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & served_p8 & served_p9 & served_p10 & served_p11 & served_p12 & !(Y(O(served_p13 | served_p14 | served_p15 | served_p16 | served_p17 | served_p18 | served_p19 | served_p20 | served_p21 | served_p22 | served_p23 | served_p24 | served_p25 | served_p26)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23))) & !(O(boarded_p15 & (boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24))) & !(O(boarded_p16 & (boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25))) & !(O(boarded_p17 & (boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26))) & !(O(boarded_p18 & (boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p0))) & !(O(boarded_p19 & (boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p0 | boarded_p1))) & !(O(boarded_p20 & (boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p21 & (boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p22 & (boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p23 & (boarded_p24 | boarded_p25 | boarded_p26 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p24 & (boarded_p25 | boarded_p26 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p25 & (boarded_p26 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p26 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8)))", - "s28-0": "O(served_p14 & served_p15 & served_p16 & served_p17 & served_p18 & served_p19 & served_p20 & served_p21 & served_p22 & served_p23 & served_p24 & served_p25 & served_p26 & served_p27) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & served_p8 & served_p9 & served_p10 & served_p11 & served_p12 & served_p13 & !(Y(O(served_p14 | served_p15 | served_p16 | served_p17 | served_p18 | served_p19 | served_p20 | served_p21 | served_p22 | served_p23 | served_p24 | served_p25 | served_p26 | served_p27)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23))) & !(O(boarded_p15 & (boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24))) & !(O(boarded_p16 & (boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25))) & !(O(boarded_p17 & (boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26))) & !(O(boarded_p18 & (boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27))) & !(O(boarded_p19 & (boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p0))) & !(O(boarded_p20 & (boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p0 | boarded_p1))) & !(O(boarded_p21 & (boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p22 & (boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p23 & (boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p24 & (boarded_p25 | boarded_p26 | boarded_p27 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p25 & (boarded_p26 | boarded_p27 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p26 & (boarded_p27 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p27 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8)))", - "s29-0": "O(served_p14 & served_p15 & served_p16 & served_p17 & served_p18 & served_p19 & served_p20 & served_p21 & served_p22 & served_p23 & served_p24 & served_p25 & served_p26 & served_p27 & served_p28) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & served_p8 & served_p9 & served_p10 & served_p11 & served_p12 & served_p13 & !(Y(O(served_p14 | served_p15 | served_p16 | served_p17 | served_p18 | served_p19 | served_p20 | served_p21 | served_p22 | served_p23 | served_p24 | served_p25 | served_p26 | served_p27 | served_p28)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23))) & !(O(boarded_p15 & (boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24))) & !(O(boarded_p16 & (boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25))) & !(O(boarded_p17 & (boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26))) & !(O(boarded_p18 & (boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27))) & !(O(boarded_p19 & (boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p28))) & !(O(boarded_p20 & (boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p28 | boarded_p0))) & !(O(boarded_p21 & (boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p28 | boarded_p0 | boarded_p1))) & !(O(boarded_p22 & (boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p28 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p23 & (boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p28 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p24 & (boarded_p25 | boarded_p26 | boarded_p27 | boarded_p28 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p25 & (boarded_p26 | boarded_p27 | boarded_p28 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p26 & (boarded_p27 | boarded_p28 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p27 & (boarded_p28 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p28 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8)))", - "s30-0": "O(served_p15 & served_p16 & served_p17 & served_p18 & served_p19 & served_p20 & served_p21 & served_p22 & served_p23 & served_p24 & served_p25 & served_p26 & served_p27 & served_p28 & served_p29) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & served_p8 & served_p9 & served_p10 & served_p11 & served_p12 & served_p13 & served_p14 & !(Y(O(served_p15 | served_p16 | served_p17 | served_p18 | served_p19 | served_p20 | served_p21 | served_p22 | served_p23 | served_p24 | served_p25 | served_p26 | served_p27 | served_p28 | served_p29)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24))) & !(O(boarded_p15 & (boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25))) & !(O(boarded_p16 & (boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26))) & !(O(boarded_p17 & (boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27))) & !(O(boarded_p18 & (boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p28))) & !(O(boarded_p19 & (boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p28 | boarded_p29))) & !(O(boarded_p20 & (boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p28 | boarded_p29 | boarded_p0))) & !(O(boarded_p21 & (boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p28 | boarded_p29 | boarded_p0 | boarded_p1))) & !(O(boarded_p22 & (boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p28 | boarded_p29 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p23 & (boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p28 | boarded_p29 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p24 & (boarded_p25 | boarded_p26 | boarded_p27 | boarded_p28 | boarded_p29 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p25 & (boarded_p26 | boarded_p27 | boarded_p28 | boarded_p29 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p26 & (boarded_p27 | boarded_p28 | boarded_p29 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p27 & (boarded_p28 | boarded_p29 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p28 & (boarded_p29 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p29 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9)))" + "s2-0": "O(\"served p1\") & O(\"served p0\" & !(Y(O(\"served p1\"))))", + "s3-0": "O(\"served p1\" & \"served p2\") & O(\"served p0\" & !(Y(O(\"served p1\" | \"served p2\")))) & !(O(\"boarded p0\" & \"boarded p1\")) & !(O(\"boarded p1\" & \"boarded p2\")) & !(O(\"boarded p2\" & \"boarded p0\"))", + "s4-0": "O(\"served p2\" & \"served p3\") & O(\"served p0\" & \"served p1\" & !(Y(O(\"served p2\" | \"served p3\")))) & !(O(\"boarded p0\" & \"boarded p1\")) & !(O(\"boarded p1\" & \"boarded p2\")) & !(O(\"boarded p2\" & \"boarded p3\")) & !(O(\"boarded p3\" & \"boarded p0\"))", + "s5-0": "O(\"served p2\" & \"served p3\" & \"served p4\") & O(\"served p0\" & \"served p1\" & !(Y(O(\"served p2\" | \"served p3\" | \"served p4\")))) & !(O(\"boarded p0\" & \"boarded p1\")) & !(O(\"boarded p1\" & \"boarded p2\")) & !(O(\"boarded p2\" & \"boarded p3\")) & !(O(\"boarded p3\" & \"boarded p4\")) & !(O(\"boarded p4\" & \"boarded p0\"))", + "s6-0": "O(\"served p3\" & \"served p4\" & \"served p5\") & O(\"served p0\" & \"served p1\" & \"served p2\" & !(Y(O(\"served p3\" | \"served p4\" | \"served p5\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p0\"))) & !(O(\"boarded p5\" & (\"boarded p0\" | \"boarded p1\")))", + "s7-0": "O(\"served p3\" & \"served p4\" & \"served p5\" & \"served p6\") & O(\"served p0\" & \"served p1\" & \"served p2\" & !(Y(O(\"served p3\" | \"served p4\" | \"served p5\" | \"served p6\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p0\"))) & !(O(\"boarded p6\" & (\"boarded p0\" | \"boarded p1\")))", + "s8-0": "O(\"served p4\" & \"served p5\" & \"served p6\" & \"served p7\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & !(Y(O(\"served p4\" | \"served p5\" | \"served p6\" | \"served p7\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p0\"))) & !(O(\"boarded p7\" & (\"boarded p0\" | \"boarded p1\")))", + "s9-0": "O(\"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & !(Y(O(\"served p4\" | \"served p5\" | \"served p6\" | \"served p7\" | \"served p8\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p0\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p8\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\")))", + "s10-0": "O(\"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & \"served p9\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & !(Y(O(\"served p5\" | \"served p6\" | \"served p7\" | \"served p8\" | \"served p9\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p0\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p9\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\")))", + "s11-0": "O(\"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & \"served p10\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & !(Y(O(\"served p5\" | \"served p6\" | \"served p7\" | \"served p8\" | \"served p9\" | \"served p10\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p0\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p10\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\")))", + "s12-0": "O(\"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & \"served p10\" & \"served p11\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & !(Y(O(\"served p6\" | \"served p7\" | \"served p8\" | \"served p9\" | \"served p10\" | \"served p11\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p0\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p11\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\")))", + "s13-0": "O(\"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & \"served p10\" & \"served p11\" & \"served p12\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & !(Y(O(\"served p6\" | \"served p7\" | \"served p8\" | \"served p9\" | \"served p10\" | \"served p11\" | \"served p12\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p0\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p12\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\")))", + "s14-0": "O(\"served p7\" & \"served p8\" & \"served p9\" & \"served p10\" & \"served p11\" & \"served p12\" & \"served p13\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & !(Y(O(\"served p7\" | \"served p8\" | \"served p9\" | \"served p10\" | \"served p11\" | \"served p12\" | \"served p13\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p0\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p13\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\")))", + "s15-0": "O(\"served p7\" & \"served p8\" & \"served p9\" & \"served p10\" & \"served p11\" & \"served p12\" & \"served p13\" & \"served p14\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & !(Y(O(\"served p7\" | \"served p8\" | \"served p9\" | \"served p10\" | \"served p11\" | \"served p12\" | \"served p13\" | \"served p14\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p0\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p14\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\")))", + "s16-0": "O(\"served p8\" & \"served p9\" & \"served p10\" & \"served p11\" & \"served p12\" & \"served p13\" & \"served p14\" & \"served p15\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & !(Y(O(\"served p8\" | \"served p9\" | \"served p10\" | \"served p11\" | \"served p12\" | \"served p13\" | \"served p14\" | \"served p15\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p0\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p15\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\")))", + "s17-0": "O(\"served p8\" & \"served p9\" & \"served p10\" & \"served p11\" & \"served p12\" & \"served p13\" & \"served p14\" & \"served p15\" & \"served p16\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & !(Y(O(\"served p8\" | \"served p9\" | \"served p10\" | \"served p11\" | \"served p12\" | \"served p13\" | \"served p14\" | \"served p15\" | \"served p16\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p0\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p16\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\")))", + "s18-0": "O(\"served p9\" & \"served p10\" & \"served p11\" & \"served p12\" & \"served p13\" & \"served p14\" & \"served p15\" & \"served p16\" & \"served p17\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & !(Y(O(\"served p9\" | \"served p10\" | \"served p11\" | \"served p12\" | \"served p13\" | \"served p14\" | \"served p15\" | \"served p16\" | \"served p17\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p0\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p17\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p16\" & (\"boarded p17\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p17\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\")))", + "s19-0": "O(\"served p9\" & \"served p10\" & \"served p11\" & \"served p12\" & \"served p13\" & \"served p14\" & \"served p15\" & \"served p16\" & \"served p17\" & \"served p18\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & !(Y(O(\"served p9\" | \"served p10\" | \"served p11\" | \"served p12\" | \"served p13\" | \"served p14\" | \"served p15\" | \"served p16\" | \"served p17\" | \"served p18\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p0\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p16\" & (\"boarded p17\" | \"boarded p18\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p17\" & (\"boarded p18\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p18\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\")))", + "s20-0": "O(\"served p10\" & \"served p11\" & \"served p12\" & \"served p13\" & \"served p14\" & \"served p15\" & \"served p16\" & \"served p17\" & \"served p18\" & \"served p19\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & !(Y(O(\"served p10\" | \"served p11\" | \"served p12\" | \"served p13\" | \"served p14\" | \"served p15\" | \"served p16\" | \"served p17\" | \"served p18\" | \"served p19\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p0\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p16\" & (\"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p17\" & (\"boarded p18\" | \"boarded p19\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p18\" & (\"boarded p19\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p19\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\")))", + "s21-0": "O(\"served p10\" & \"served p11\" & \"served p12\" & \"served p13\" & \"served p14\" & \"served p15\" & \"served p16\" & \"served p17\" & \"served p18\" & \"served p19\" & \"served p20\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & !(Y(O(\"served p10\" | \"served p11\" | \"served p12\" | \"served p13\" | \"served p14\" | \"served p15\" | \"served p16\" | \"served p17\" | \"served p18\" | \"served p19\" | \"served p20\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p0\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p16\" & (\"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p17\" & (\"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p18\" & (\"boarded p19\" | \"boarded p20\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p19\" & (\"boarded p20\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p20\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\")))", + "s22-0": "O(\"served p11\" & \"served p12\" & \"served p13\" & \"served p14\" & \"served p15\" & \"served p16\" & \"served p17\" & \"served p18\" & \"served p19\" & \"served p20\" & \"served p21\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & \"served p10\" & !(Y(O(\"served p11\" | \"served p12\" | \"served p13\" | \"served p14\" | \"served p15\" | \"served p16\" | \"served p17\" | \"served p18\" | \"served p19\" | \"served p20\" | \"served p21\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p0\"))) & !(O(\"boarded p16\" & (\"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p17\" & (\"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p18\" & (\"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p19\" & (\"boarded p20\" | \"boarded p21\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p20\" & (\"boarded p21\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p21\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\")))", + "s23-0": "O(\"served p11\" & \"served p12\" & \"served p13\" & \"served p14\" & \"served p15\" & \"served p16\" & \"served p17\" & \"served p18\" & \"served p19\" & \"served p20\" & \"served p21\" & \"served p22\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & \"served p10\" & !(Y(O(\"served p11\" | \"served p12\" | \"served p13\" | \"served p14\" | \"served p15\" | \"served p16\" | \"served p17\" | \"served p18\" | \"served p19\" | \"served p20\" | \"served p21\" | \"served p22\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\"))) & !(O(\"boarded p16\" & (\"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p0\"))) & !(O(\"boarded p17\" & (\"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p18\" & (\"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p19\" & (\"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p20\" & (\"boarded p21\" | \"boarded p22\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p21\" & (\"boarded p22\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p22\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\")))", + "s24-0": "O(\"served p12\" & \"served p13\" & \"served p14\" & \"served p15\" & \"served p16\" & \"served p17\" & \"served p18\" & \"served p19\" & \"served p20\" & \"served p21\" & \"served p22\" & \"served p23\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & \"served p10\" & \"served p11\" & !(Y(O(\"served p12\" | \"served p13\" | \"served p14\" | \"served p15\" | \"served p16\" | \"served p17\" | \"served p18\" | \"served p19\" | \"served p20\" | \"served p21\" | \"served p22\" | \"served p23\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\"))) & !(O(\"boarded p16\" & (\"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p0\"))) & !(O(\"boarded p17\" & (\"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p18\" & (\"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p19\" & (\"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p20\" & (\"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p21\" & (\"boarded p22\" | \"boarded p23\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p22\" & (\"boarded p23\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p23\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\")))", + "s25-0": "O(\"served p12\" & \"served p13\" & \"served p14\" & \"served p15\" & \"served p16\" & \"served p17\" & \"served p18\" & \"served p19\" & \"served p20\" & \"served p21\" & \"served p22\" & \"served p23\" & \"served p24\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & \"served p10\" & \"served p11\" & !(Y(O(\"served p12\" | \"served p13\" | \"served p14\" | \"served p15\" | \"served p16\" | \"served p17\" | \"served p18\" | \"served p19\" | \"served p20\" | \"served p21\" | \"served p22\" | \"served p23\" | \"served p24\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\"))) & !(O(\"boarded p16\" & (\"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\"))) & !(O(\"boarded p17\" & (\"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p0\"))) & !(O(\"boarded p18\" & (\"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p19\" & (\"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p20\" & (\"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p21\" & (\"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p22\" & (\"boarded p23\" | \"boarded p24\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p23\" & (\"boarded p24\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p24\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\")))", + "s26-0": "O(\"served p13\" & \"served p14\" & \"served p15\" & \"served p16\" & \"served p17\" & \"served p18\" & \"served p19\" & \"served p20\" & \"served p21\" & \"served p22\" & \"served p23\" & \"served p24\" & \"served p25\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & \"served p10\" & \"served p11\" & \"served p12\" & !(Y(O(\"served p13\" | \"served p14\" | \"served p15\" | \"served p16\" | \"served p17\" | \"served p18\" | \"served p19\" | \"served p20\" | \"served p21\" | \"served p22\" | \"served p23\" | \"served p24\" | \"served p25\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\"))) & !(O(\"boarded p16\" & (\"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\"))) & !(O(\"boarded p17\" & (\"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\"))) & !(O(\"boarded p18\" & (\"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p0\"))) & !(O(\"boarded p19\" & (\"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p20\" & (\"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p21\" & (\"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p22\" & (\"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p23\" & (\"boarded p24\" | \"boarded p25\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p24\" & (\"boarded p25\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p25\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\")))", + "s27-0": "O(\"served p13\" & \"served p14\" & \"served p15\" & \"served p16\" & \"served p17\" & \"served p18\" & \"served p19\" & \"served p20\" & \"served p21\" & \"served p22\" & \"served p23\" & \"served p24\" & \"served p25\" & \"served p26\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & \"served p10\" & \"served p11\" & \"served p12\" & !(Y(O(\"served p13\" | \"served p14\" | \"served p15\" | \"served p16\" | \"served p17\" | \"served p18\" | \"served p19\" | \"served p20\" | \"served p21\" | \"served p22\" | \"served p23\" | \"served p24\" | \"served p25\" | \"served p26\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\"))) & !(O(\"boarded p16\" & (\"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\"))) & !(O(\"boarded p17\" & (\"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\"))) & !(O(\"boarded p18\" & (\"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p0\"))) & !(O(\"boarded p19\" & (\"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p20\" & (\"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p21\" & (\"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p22\" & (\"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p23\" & (\"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p24\" & (\"boarded p25\" | \"boarded p26\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p25\" & (\"boarded p26\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p26\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\")))", + "s28-0": "O(\"served p14\" & \"served p15\" & \"served p16\" & \"served p17\" & \"served p18\" & \"served p19\" & \"served p20\" & \"served p21\" & \"served p22\" & \"served p23\" & \"served p24\" & \"served p25\" & \"served p26\" & \"served p27\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & \"served p10\" & \"served p11\" & \"served p12\" & \"served p13\" & !(Y(O(\"served p14\" | \"served p15\" | \"served p16\" | \"served p17\" | \"served p18\" | \"served p19\" | \"served p20\" | \"served p21\" | \"served p22\" | \"served p23\" | \"served p24\" | \"served p25\" | \"served p26\" | \"served p27\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\"))) & !(O(\"boarded p16\" & (\"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\"))) & !(O(\"boarded p17\" & (\"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\"))) & !(O(\"boarded p18\" & (\"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\"))) & !(O(\"boarded p19\" & (\"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p0\"))) & !(O(\"boarded p20\" & (\"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p21\" & (\"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p22\" & (\"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p23\" & (\"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p24\" & (\"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p25\" & (\"boarded p26\" | \"boarded p27\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p26\" & (\"boarded p27\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p27\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\")))", + "s29-0": "O(\"served p14\" & \"served p15\" & \"served p16\" & \"served p17\" & \"served p18\" & \"served p19\" & \"served p20\" & \"served p21\" & \"served p22\" & \"served p23\" & \"served p24\" & \"served p25\" & \"served p26\" & \"served p27\" & \"served p28\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & \"served p10\" & \"served p11\" & \"served p12\" & \"served p13\" & !(Y(O(\"served p14\" | \"served p15\" | \"served p16\" | \"served p17\" | \"served p18\" | \"served p19\" | \"served p20\" | \"served p21\" | \"served p22\" | \"served p23\" | \"served p24\" | \"served p25\" | \"served p26\" | \"served p27\" | \"served p28\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\"))) & !(O(\"boarded p16\" & (\"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\"))) & !(O(\"boarded p17\" & (\"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\"))) & !(O(\"boarded p18\" & (\"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\"))) & !(O(\"boarded p19\" & (\"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p28\"))) & !(O(\"boarded p20\" & (\"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p28\" | \"boarded p0\"))) & !(O(\"boarded p21\" & (\"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p28\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p22\" & (\"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p28\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p23\" & (\"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p28\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p24\" & (\"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p28\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p25\" & (\"boarded p26\" | \"boarded p27\" | \"boarded p28\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p26\" & (\"boarded p27\" | \"boarded p28\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p27\" & (\"boarded p28\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p28\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\")))", + "s30-0": "O(\"served p15\" & \"served p16\" & \"served p17\" & \"served p18\" & \"served p19\" & \"served p20\" & \"served p21\" & \"served p22\" & \"served p23\" & \"served p24\" & \"served p25\" & \"served p26\" & \"served p27\" & \"served p28\" & \"served p29\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & \"served p10\" & \"served p11\" & \"served p12\" & \"served p13\" & \"served p14\" & !(Y(O(\"served p15\" | \"served p16\" | \"served p17\" | \"served p18\" | \"served p19\" | \"served p20\" | \"served p21\" | \"served p22\" | \"served p23\" | \"served p24\" | \"served p25\" | \"served p26\" | \"served p27\" | \"served p28\" | \"served p29\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\"))) & !(O(\"boarded p16\" & (\"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\"))) & !(O(\"boarded p17\" & (\"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\"))) & !(O(\"boarded p18\" & (\"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p28\"))) & !(O(\"boarded p19\" & (\"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p28\" | \"boarded p29\"))) & !(O(\"boarded p20\" & (\"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p28\" | \"boarded p29\" | \"boarded p0\"))) & !(O(\"boarded p21\" & (\"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p28\" | \"boarded p29\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p22\" & (\"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p28\" | \"boarded p29\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p23\" & (\"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p28\" | \"boarded p29\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p24\" & (\"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p28\" | \"boarded p29\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p25\" & (\"boarded p26\" | \"boarded p27\" | \"boarded p28\" | \"boarded p29\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p26\" & (\"boarded p27\" | \"boarded p28\" | \"boarded p29\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p27\" & (\"boarded p28\" | \"boarded p29\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p28\" & (\"boarded p29\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p29\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\")))" } \ No newline at end of file diff --git a/tests/test_compiler/test_blocksworld_det.py b/tests/test_compiler/test_blocksworld_det.py index 2e412a3c..a99bb5a9 100644 --- a/tests/test_compiler/test_blocksworld_det.py +++ b/tests/test_compiler/test_blocksworld_det.py @@ -50,7 +50,7 @@ def make_formula(self, instance_id: int, domain: Path, problem: Path) -> str: trailing_brackets = "" for i in range(1, instance_id): last = i == instance_id - 1 - formula += f"O(on_b{i}_b{i + 1}" + (" & Y(" if not last else "") + formula += f'O("on b{i} b{i + 1}"' + (" & Y(" if not last else "") trailing_brackets += "))" if not last else ")" return formula + trailing_brackets diff --git a/tests/test_compiler/test_readme_example.py b/tests/test_compiler/test_readme_example.py index b2015447..383cf543 100644 --- a/tests/test_compiler/test_readme_example.py +++ b/tests/test_compiler/test_readme_example.py @@ -24,31 +24,18 @@ from pathlib import Path -import pytest -from pddl.logic import Predicate, constants from pddl.parser.domain import DomainParser from pddl.parser.problem import ProblemParser from pylogics.parsers import parse_pltl -from pylogics.syntax.pltl import Atomic as PLTLAtomic from plan4past.compiler import Compiler from tests.helpers.constants import EXAMPLES_DIR from tests.helpers.misc import check_compilation -@pytest.mark.parametrize( - "from_atoms_to_fluent", - [ - None, - { - PLTLAtomic("on_b_a"): Predicate("on", *constants("b a")), - PLTLAtomic("ontable_c"): Predicate("ontable", *constants("c")), - }, - ], -) -def test_readme_example(val, default_planner, from_atoms_to_fluent) -> None: +def test_readme_example(val, default_planner) -> None: """Test the example from the README.""" - formula = "on_b_a & O(ontable_c)" + formula = '"on b a" & O("ontable c")' domain_parser = DomainParser() problem_parser = ProblemParser() @@ -59,9 +46,7 @@ def test_readme_example(val, default_planner, from_atoms_to_fluent) -> None: problem = problem_parser(pddl_example_problem_path.read_text(encoding="utf-8")) goal = parse_pltl(formula) - compiler = Compiler( - domain, problem, goal, from_atoms_to_fluent=from_atoms_to_fluent - ) + compiler = Compiler(domain, problem, goal) compiler.compile() compiled_domain, compiled_problem = compiler.result diff --git a/tests/test_helpers/test_utils.py b/tests/test_helpers/test_utils.py index 18237ef1..755f1735 100644 --- a/tests/test_helpers/test_utils.py +++ b/tests/test_helpers/test_utils.py @@ -22,37 +22,15 @@ """This module contains tests for the plan4past.helpers.utils module.""" import pytest -from pddl.logic import Predicate, constants -from pylogics.syntax.pltl import Atomic as PLTLAtomic -from pylogics.syntax.pltl import Before, Since from plan4past.helpers.utils import ( add_val_prefix, check_, - default_mapping, remove_before_prefix, remove_val_prefix, ) -def test_default_mapping() -> None: - """Test the default mapping function.""" - p_a_b = PLTLAtomic("p_a_b") - p_b_c = PLTLAtomic("p_b_c") - p_c_d = PLTLAtomic("p_c_d") - p2 = PLTLAtomic("p2") - before_p_a_b = Before(p_a_b) - p_b_c_since_p_c_d = Since(p_b_c, p_c_d) - - result = default_mapping(before_p_a_b & p_b_c_since_p_c_d & p2) - assert result == { - p_a_b: Predicate("p", *constants("a b")), - p_b_c: Predicate("p", *constants("b c")), - p_c_d: Predicate("p", *constants("c d")), - p2: Predicate("p2"), - } - - def test_val_prefix() -> None: """Test the add_val_prefix function.""" assert add_val_prefix("Y-foo") == "val-Y-foo" diff --git a/tests/test_utils/test_derived_visitor.py b/tests/test_utils/test_derived_visitor.py index aa299c92..6b050df0 100644 --- a/tests/test_utils/test_derived_visitor.py +++ b/tests/test_utils/test_derived_visitor.py @@ -24,7 +24,6 @@ from typing import Set import pytest -from pddl.logic import Constant from pddl.logic.base import And, Not, Or from pddl.logic.predicates import DerivedPredicate, Predicate from pylogics.syntax.pltl import Atomic as PLTLAtomic @@ -62,7 +61,7 @@ def test_derived_predicates_visitor_not_implemented_fail(): with pytest.raises( NotImplementedError, match="handler not implemented for object " ): - derived_predicates(1, {}) + derived_predicates(1) def test_derived_predicates_visitor_true(): @@ -70,7 +69,7 @@ def test_derived_predicates_visitor_true(): val = Predicate(add_val_prefix("true")) expected = {DerivedPredicate(val, And())} - actual = derived_predicates(PropositionalTrue(), {}) + actual = derived_predicates(PropositionalTrue()) assert _eq(actual, expected) @@ -79,7 +78,7 @@ def test_derived_predicates_visitor_false(): val = Predicate(add_val_prefix("false")) expected = {DerivedPredicate(val, Or())} - actual = derived_predicates(PropositionalFalse(), {}) + actual = derived_predicates(PropositionalFalse()) assert _eq(actual, expected) @@ -87,10 +86,10 @@ def test_derived_predicates_visitor_atomic(): """Test the derived predicates visitor for the atomic formula.""" a = PLTLAtomic("a") val = Predicate(add_val_prefix("a")) - condition = Predicate("p", Constant("a")) + condition = Predicate("a") expected = {DerivedPredicate(val, condition)} - actual = derived_predicates(a, {a: condition}) + actual = derived_predicates(a) assert _eq(actual, expected) @@ -99,8 +98,8 @@ def test_derived_predicates_visitor_and(): a = PLTLAtomic("a") b = PLTLAtomic("b") - condition_a = Predicate("p", Constant("a")) - condition_b = Predicate("p", Constant("b")) + condition_a = Predicate("a") + condition_b = Predicate("b") val = Predicate(add_val_prefix("a-and-b")) val_a = Predicate(add_val_prefix("a")) @@ -114,7 +113,7 @@ def test_derived_predicates_visitor_and(): DerivedPredicate(val_b, condition_b), } - actual = derived_predicates(a & b, {a: condition_a, b: condition_b}) + actual = derived_predicates(a & b) assert _eq(actual, expected) @@ -123,8 +122,8 @@ def test_derived_predicates_visitor_or(): a = PLTLAtomic("a") b = PLTLAtomic("b") - condition_a = Predicate("p", Constant("a")) - condition_b = Predicate("p", Constant("b")) + condition_a = Predicate("a") + condition_b = Predicate("b") val = Predicate(add_val_prefix("a-or-b")) val_a = Predicate(add_val_prefix("a")) @@ -138,7 +137,7 @@ def test_derived_predicates_visitor_or(): DerivedPredicate(val_b, condition_b), } - actual = derived_predicates(a | b, {a: condition_a, b: condition_b}) + actual = derived_predicates(a | b) assert _eq(actual, expected) @@ -146,7 +145,7 @@ def test_derived_predicates_visitor_not(): """Test the derived predicates visitor for the not formula.""" a = PLTLAtomic("a") - condition_a = Predicate("p", Constant("a")) + condition_a = Predicate("a") val = Predicate(add_val_prefix("not-a")) val_a = Predicate(add_val_prefix("a")) @@ -155,7 +154,7 @@ def test_derived_predicates_visitor_not(): expected = {DerivedPredicate(val, condition), DerivedPredicate(val_a, condition_a)} - actual = derived_predicates(~a, {a: condition_a}) + actual = derived_predicates(~a) assert _eq(actual, expected) @@ -164,7 +163,7 @@ def test_derived_predicates_visitor_before(): a = PLTLAtomic("a") Ya = Before(a) - condition_a = Predicate("p", Constant("a")) + condition_a = Predicate("a") val = Predicate(add_val_prefix("Ya")) val_a = Predicate(add_val_prefix("a")) @@ -173,7 +172,7 @@ def test_derived_predicates_visitor_before(): expected = {DerivedPredicate(val, condition), DerivedPredicate(val_a, condition_a)} - actual = derived_predicates(Ya, {a: condition_a}) + actual = derived_predicates(Ya) assert _eq(actual, expected) @@ -192,9 +191,9 @@ def test_derived_predicates_visitor_since(): Y_a_since_b_since_c = Predicate("Y-a-S-b-S-c") Y_b_since_c = Predicate("Y-b-S-c") - condition_a = Predicate("p", Constant("a")) - condition_b = Predicate("p", Constant("b")) - condition_c = Predicate("p", Constant("c")) + condition_a = Predicate("a") + condition_b = Predicate("b") + condition_c = Predicate("c") condition_b_since_c = Or(val_c, And(val_b, Y_b_since_c)) condition_a_since_b_since_c = Or(val_b_since_c, And(val_a, Y_a_since_b_since_c)) @@ -206,9 +205,7 @@ def test_derived_predicates_visitor_since(): DerivedPredicate(val_c, condition_c), } - actual = derived_predicates( - a_since_b_since_c, {a: condition_a, b: condition_b, c: condition_c} - ) + actual = derived_predicates(a_since_b_since_c) assert _eq(actual, expected) @@ -221,7 +218,7 @@ def test_derived_predicates_visitor_once(): val_once_a = Predicate(add_val_prefix("Oa")) Y_once_a = Predicate("Y-Oa") - condition_a = Predicate("p", Constant("a")) + condition_a = Predicate("a") condition_once_a = Or(val_a, Y_once_a) expected = { @@ -229,5 +226,5 @@ def test_derived_predicates_visitor_once(): DerivedPredicate(val_once_a, condition_once_a), } - actual = derived_predicates(once_a, {a: condition_a}) + actual = derived_predicates(once_a) assert _eq(actual, expected) diff --git a/tests/test_utils/test_mapping_parser.py b/tests/test_utils/test_mapping_parser.py deleted file mode 100644 index a9944f7a..00000000 --- a/tests/test_utils/test_mapping_parser.py +++ /dev/null @@ -1,168 +0,0 @@ -# -*- coding: utf-8 -*- -# -# Copyright 2021 -- 2023 WhiteMech -# -# ------------------------------ -# -# This file is part of Plan4Past. -# -# Plan4Past is free software: you can redistribute it and/or modify -# it under the terms of the GNU Lesser General Public License as published by -# the Free Software Foundation, either version 3 of the License, or -# (at your option) any later version. -# -# Plan4Past is distributed in the hope that it will be useful, -# but WITHOUT ANY WARRANTY; without even the implied warranty of -# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -# GNU Lesser General Public License for more details. -# -# You should have received a copy of the GNU Lesser General Public License -# along with Plan4Past. If not, see . -# - -"""This module contains tests for the plan4past.utils.mapping_parser module.""" -from textwrap import dedent - -import pytest -from pddl.logic import Constant, Predicate, constants -from pylogics.syntax.pltl import Atomic as PLTLAtomic -from pylogics.syntax.pltl import FalseFormula as PLTLFalse -from pylogics.syntax.pltl import TrueFormula as PLTLTrue - -from plan4past.utils.mapping_parser import MappingParserError, mapping_parser -from tests.helpers.constants import EXAMPLE_MAP_FILE - -_on_b_a = PLTLAtomic("on_b_a") -_ontable_c = PLTLAtomic("ontable_c") - -_pddl_on_b_a = Predicate("on", *constants("b a")) -_pddl_ontable_c = Predicate("ontable", Constant("c")) - - -@pytest.mark.parametrize( - "formula,expected_mapping", - [ - (PLTLTrue(), {}), - (PLTLFalse(), {}), - (_on_b_a, {_on_b_a: _pddl_on_b_a}), - (_ontable_c, {_ontable_c: _pddl_ontable_c}), - (_on_b_a & _ontable_c, {_on_b_a: _pddl_on_b_a, _ontable_c: _pddl_ontable_c}), - ], -) -def test_mapping_parser_successful_case(formula, expected_mapping): - """Test the mapping parser with the example map file.""" - actual_mapping = mapping_parser(EXAMPLE_MAP_FILE.read_text(), formula) - assert actual_mapping == expected_mapping - - -def test_mapping_parser_empty_file(): - """Test the mapping parser when the file is empty.""" - assert not mapping_parser("", PLTLTrue()) - - -def test_mapping_parser_empty_lines(): - """Test the mapping parser with empty lines.""" - assert not mapping_parser("\n\n", PLTLTrue()) - - -def test_mapping_parser_with_comments(): - """Test the mapping parser with comments.""" - assert mapping_parser(";;;;\n;\non_b_a,on b a", _on_b_a) == {_on_b_a: _pddl_on_b_a} - - -def test_mapping_parser_when_row_has_no_comma(): - """Test the mapping parser when a row is invalid (has no comma).""" - with pytest.raises( - MappingParserError, - match="invalid mapping at row 0: expected a mapping of the form ','", - ): - mapping_parser( - "invalid_row\n", - PLTLTrue(), - ) - - -def test_mapping_parser_when_row_has_more_than_one_comma(): - """Test the mapping parser when a row is invalid (has more than two commas).""" - with pytest.raises( - MappingParserError, - match="invalid mapping at row 0: expected a mapping of the form ','", - ): - mapping_parser( - "invalid_row,invalid_row,\n", - PLTLTrue(), - ) - - -def test_mapping_parser_bad_symbol_format(): - """Test the mapping parser when a row is invalid (bad symbol format).""" - with pytest.raises( - MappingParserError, - match="invalid mapping at row 0: symbol cannot be empty string and must match the regex ", - ): - mapping_parser( - "not a valid symbol,some_predicate\n", - PLTLTrue(), - ) - - -def test_mapping_parser_empty_predicate_name(): - """Test the mapping parser when a row is invalid (empty predicate name).""" - with pytest.raises( - MappingParserError, - match="invalid mapping at row 0: predicate cannot be empty string", - ): - mapping_parser( - "some_symbol,\n", - PLTLTrue(), - ) - - -def test_mapping_parser_invalid_predicate_name(): - """Test the mapping parser when a row is invalid (invalid predicate name).""" - with pytest.raises( - MappingParserError, - match=r"invalid mapping at row 0: got an invalid name for a predicate: 'not!'\. It must match the regex .*", - ): - mapping_parser( - "some_symbol,not! a valid predicate\n", - PLTLTrue(), - ) - - -def test_mapping_parser_invalid_constant_name(): - """Test the mapping parser when a row is invalid (invalid constant name).""" - with pytest.raises( - MappingParserError, - match=r"invalid mapping at row 0: got an invalid constant: Value 'wrong-constant-name!' " - r"does not match the regular expression .*", - ): - mapping_parser( - "some_symbol,predicate wrong-constant-name!\n", - PLTLTrue(), - ) - - -def test_mapping_parser_in_case_of_unmapped_symbols(): - """Test the mapping parser when a symbol is not mapped.""" - with pytest.raises( - MappingParserError, - match=r"invalid mapping: the following symbols of the formula are not mapped: {'a|b', 'b|a'}", - ): - mapping_parser( - dedent( - """\ - some_symbol,predicate some_constant - """ - ), - PLTLAtomic("a") & PLTLAtomic("b") & PLTLTrue(), - ) - - -def test_mapping_parser_symbol_occurs_more_than_once(): - """Test the mapping parser when a symbol occurs more than once.""" - with pytest.raises( - MappingParserError, - match="invalid mapping at row 1: symbol 'on_b_a' is mapped multiple times", - ): - mapping_parser("on_b_a,on b a\non_b_a,on b a", _on_b_a) diff --git a/tests/test_utils/test_rewrite_formula_visitor.py b/tests/test_utils/test_rewrite_formula_visitor.py index 2bd8a6fc..7a5dbcbe 100644 --- a/tests/test_utils/test_rewrite_formula_visitor.py +++ b/tests/test_utils/test_rewrite_formula_visitor.py @@ -58,75 +58,75 @@ def test_rewrite_formula_visitor_false(): def test_rewrite_formula_visitor_atomic(): """Test the rewrite formula visitor for the atomic formula.""" - a = PLTLAtomic("a") + a = PLTLAtomic('"a"') assert rewrite(a) == a def test_rewrite_formula_visitor_and(): """Test the rewrite formula visitor for the and formula.""" - a = PLTLAtomic("a") - b = PLTLAtomic("b") - c = PLTLAtomic("c") - d = PLTLAtomic("d") + a = PLTLAtomic('"a"') + b = PLTLAtomic('"b"') + c = PLTLAtomic('"c"') + d = PLTLAtomic('"d"') assert rewrite(PLTLImplies(a, b) & PLTLImplies(c, d)) == (~a | b) & (~c | d) def test_rewrite_formula_visitor_or(): """Test the rewrite formula visitor for the or formula.""" - a = PLTLAtomic("a") - b = PLTLAtomic("b") - c = PLTLAtomic("c") - d = PLTLAtomic("d") + a = PLTLAtomic('"a"') + b = PLTLAtomic('"b"') + c = PLTLAtomic('"c"') + d = PLTLAtomic('"d"') assert rewrite(PLTLImplies(a, b) | PLTLImplies(c, d)) == (~a | b) | (~c | d) def test_rewrite_formula_visitor_not(): """Test the rewrite formula visitor for the not formula.""" - a = PLTLAtomic("a") - b = PLTLAtomic("b") + a = PLTLAtomic('"a"') + b = PLTLAtomic('"b"') assert rewrite(~PLTLImplies(a, b)) == ~(~a | b) def test_rewrite_formula_visitor_implies(): """Test the rewrite formula visitor for the implies formula.""" - a = PLTLAtomic("a") - b = PLTLAtomic("b") + a = PLTLAtomic('"a"') + b = PLTLAtomic('"b"') assert rewrite(PLTLImplies(a, b)) == (~a | b) def test_rewrite_formula_visitor_equivalence(): """Test the rewrite formula visitor for the equivalence formula.""" - a = PLTLAtomic("a") - b = PLTLAtomic("b") + a = PLTLAtomic('"a"') + b = PLTLAtomic('"b"') assert rewrite(PLTLEquivalence(a, b)) == ((a & b) | (~a & ~b)) def test_rewrite_formula_visitor_before(): """Test the rewrite formula visitor for the before formula.""" - a = PLTLAtomic("a") + a = PLTLAtomic('"a"') before_a = Before(a) assert rewrite(before_a) == before_a def test_rewrite_formula_visitor_since(): """Test the rewrite formula visitor for the before formula.""" - a = PLTLAtomic("a") - b = PLTLAtomic("b") - c = PLTLAtomic("c") - d = PLTLAtomic("d") + a = PLTLAtomic('"a"') + b = PLTLAtomic('"b"') + c = PLTLAtomic('"c"') + d = PLTLAtomic('"d"') a_since_b_since_c_implies_d = Since(a, b, PLTLImplies(c, d)) assert rewrite(a_since_b_since_c_implies_d) == Since(a, Since(b, (~c | d))) def test_rewrite_formula_visitor_once(): """Test the rewrite formula visitor for the once formula.""" - a = PLTLAtomic("a") + a = PLTLAtomic('"a"') once_a = Once(a) assert rewrite(once_a) == once_a def test_rewrite_formula_visitor_historically(): """Test the rewrite formula visitor for the historically formula.""" - a = PLTLAtomic("a") + a = PLTLAtomic('"a"') historically_a = Historically(a) assert rewrite(historically_a) == ~Once(~a) From 1559f0ecd987c9a0984355b7054d05874eebd44e Mon Sep 17 00:00:00 2001 From: Marco Favorito Date: Sun, 9 Jul 2023 22:50:19 +0200 Subject: [PATCH 2/3] fix: change prefix to val__; check no atom starts with it We now check if the prefix 'val' is in the atom name. This is because after the compilation there might be conflicts in the val predicate names. Consider the following example: '"p a b" & val-p-a-b' The formula is compiled as follows: "p a b" -> 'val-p-a-b' (:derived (val-p-a-b) (p a b)) ^ ^ derived-predicate condition (ground fluent, predicate name 'p', constants 'a' and 'b') "val-p-a-b" -> 'val-val-p-a-b' (:derived (val-val-p-a-b) (val-p-a-b)) ^ ^ derived-predicate condition (ground fluent, predicate name 'p-a-b', no constants The prefix is changed to `val__` to make the prefix less probable to occur in an atom name. --- plan4past/helpers/utils.py | 11 +++++++++-- tests/test_helpers/test_utils.py | 10 +++++----- 2 files changed, 14 insertions(+), 7 deletions(-) diff --git a/plan4past/helpers/utils.py b/plan4past/helpers/utils.py index 3175f59f..aff06719 100644 --- a/plan4past/helpers/utils.py +++ b/plan4past/helpers/utils.py @@ -29,11 +29,12 @@ _GROUND_FLUENT_REGEX = re.compile( rf"(\"({_PDDL_NAME_REGEX})( {_PDDL_NAME_REGEX})*\")|({_PDDL_NAME_REGEX})" ) +_VAL_PREFIX = "val__" def add_val_prefix(name: str): """Add the 'prime' prefix.""" - return "val-" + name.replace('"', "") + return _VAL_PREFIX + name.replace('"', "") def remove_before_prefix(name: str): @@ -49,7 +50,7 @@ def remove_before_prefix(name: str): def remove_val_prefix(name: str): """Remove the 'prime' prefix.""" - return name.replace("val-", "") if name.startswith("val-") else name + return name.replace(_VAL_PREFIX, "") if name.startswith(_VAL_PREFIX) else name def replace_symbols(name: str): @@ -104,5 +105,11 @@ def validate(symbol: str) -> None: :param symbol: the symbol """ + # check if the symbol does not start with the 'val__' prefix + if symbol.startswith(_VAL_PREFIX): + raise ValueError( + f"invalid symbol: symbol '{symbol}' cannot start with {_VAL_PREFIX}" + ) + # check if the symbol is a valid PDDL ground fluent parse_ground_fluent(symbol) diff --git a/tests/test_helpers/test_utils.py b/tests/test_helpers/test_utils.py index 755f1735..78fad0fa 100644 --- a/tests/test_helpers/test_utils.py +++ b/tests/test_helpers/test_utils.py @@ -33,10 +33,10 @@ def test_val_prefix() -> None: """Test the add_val_prefix function.""" - assert add_val_prefix("Y-foo") == "val-Y-foo" - assert add_val_prefix("Yfoo") == "val-Yfoo" - assert add_val_prefix("foo") == "val-foo" - assert add_val_prefix("Y-foo-bar") == "val-Y-foo-bar" + assert add_val_prefix("Y-foo") == "val__Y-foo" + assert add_val_prefix("Yfoo") == "val__Yfoo" + assert add_val_prefix("foo") == "val__foo" + assert add_val_prefix("Y-foo-bar") == "val__Y-foo-bar" def test_remove_before_prefix() -> None: @@ -48,7 +48,7 @@ def test_remove_before_prefix() -> None: def test_remove_val_prefix() -> None: """Test the remove_val_prefix function.""" - assert remove_val_prefix("val-foo") == "foo" + assert remove_val_prefix("val__foo") == "foo" assert remove_val_prefix("foo") == "foo" From 838f43c20d6b91338d7f713ac340985882eeeced Mon Sep 17 00:00:00 2001 From: Marco Favorito Date: Sun, 9 Jul 2023 23:40:50 +0200 Subject: [PATCH 3/3] fix: make encoding of derived predicate invertible with this change, we translate each formula special symbols (operator symbols, parenthesis etc.) into a sequence of characters that can be part of a valid derived predicate name. This means that, given a name of a derived predicate, one can simply do the inverse replacement and recover the original formula. This approach has two major drawbacks: 1) the output of the compiler is much more verbose; e.g. the formula 'Y(a)' gets translated into 'val__YLPAR__a__RPAR' 2) the new approach imposes restrictions on the allowed symbols in a PPLTL formula. E.g. symbols that start with 'VAL__' or 'Y__', or symbols that contain one of the following as substring: - "LPAR__" (left parenthesis) - "__RPAR" (right parenthesis) - "NOT__" (not symbol) - "__AND__" (and symbol) - "__OR__" (or symbol) - "__QUOTE__" (quote) are forbidden. This policy might be more conservative than needed, but in this way we should have the guarantee that the encoding is an invertible mapping (such property basically proves non-ambiguity of the encoding, because it means there is a one-to-one relationship between 'string representation of pylogics formulas' and 'string representation encoded as PDDL predicate name'). --- plan4past/compiler.py | 5 +- plan4past/helpers/utils.py | 85 ++++++++++++++----- plan4past/utils/derived_visitor.py | 11 ++- plan4past/utils/predicates_visitor.py | 6 +- tests/helpers/planutils/downward.py | 2 +- tests/test_compiler/test_blocksworld_det.py | 4 +- tests/test_helpers/test_utils.py | 14 +-- tests/test_utils/test_derived_visitor.py | 26 +++--- tests/test_utils/test_predicates_visitor.py | 8 +- .../test_utils/test_val_predicates_visitor.py | 16 ++-- 10 files changed, 116 insertions(+), 61 deletions(-) diff --git a/plan4past/compiler.py b/plan4past/compiler.py index cb9478ba..e3bef8a8 100644 --- a/plan4past/compiler.py +++ b/plan4past/compiler.py @@ -133,12 +133,13 @@ def _compile_problem(self): def _compute_whens(formula: Formula) -> Set[When]: """Compute conditional effects for formula progression.""" + formula_predicates = predicates(formula) return { When(Predicate(add_val_prefix(remove_before_prefix(p.name))), p) - for p in predicates(formula) + for p in formula_predicates }.union( When(Not(Predicate(add_val_prefix(remove_before_prefix(p.name)))), Not(p)) - for p in predicates(formula) + for p in formula_predicates ) diff --git a/plan4past/helpers/utils.py b/plan4past/helpers/utils.py index aff06719..a76028f9 100644 --- a/plan4past/helpers/utils.py +++ b/plan4past/helpers/utils.py @@ -22,6 +22,7 @@ """Miscellanea utilities.""" import re +from typing import Collection, Type from pddl.logic import Predicate, constants @@ -29,45 +30,54 @@ _GROUND_FLUENT_REGEX = re.compile( rf"(\"({_PDDL_NAME_REGEX})( {_PDDL_NAME_REGEX})*\")|({_PDDL_NAME_REGEX})" ) -_VAL_PREFIX = "val__" +VAL_PREFIX = "VAL__" +_LEFT_PAR = "LPAR__" +_RIGHT_PAR = "__RPAR" +Y_PREFIX = "Y__" +_NOT = "NOT__" +_AND = "__AND__" +_OR = "__OR__" +_QUOTE = "__QUOTE__" def add_val_prefix(name: str): """Add the 'prime' prefix.""" - return _VAL_PREFIX + name.replace('"', "") + return VAL_PREFIX + name.replace('"', _QUOTE) def remove_before_prefix(name: str): """Remove the 'Y' prefix.""" return ( - name.replace("Y-", "") - if name.startswith("Y-") - else name.replace("Y", "", 1) - if name.startswith("Y") + name.replace(Y_PREFIX, "") + if name.startswith(Y_PREFIX) + else re.sub(f"{_RIGHT_PAR}$", "", name.replace("Y" + _LEFT_PAR, "", 1)) + if name.startswith("Y" + _LEFT_PAR) else name ) def remove_val_prefix(name: str): """Remove the 'prime' prefix.""" - return name.replace(_VAL_PREFIX, "") if name.startswith(_VAL_PREFIX) else name + return name.replace(VAL_PREFIX, "") if name.startswith(VAL_PREFIX) else name def replace_symbols(name: str): """Stringify symbols.""" return ( - name.replace('"', "") - .replace("(", "") - .replace(")", "") - .replace("&", "and") - .replace("|", "or") - .replace("~", "not-") - .replace("!", "not-") + name.replace('"', _QUOTE) + .replace("(", _LEFT_PAR) + .replace(")", _RIGHT_PAR) + .replace("&", _AND) + .replace("|", _OR) + .replace("~", _NOT) + .replace("!", _NOT) .replace(" ", "-") ) -def check_(condition: bool, message: str = "") -> None: +def check_( + condition: bool, message: str = "", exception_cls: Type[Exception] = AssertionError +) -> None: """ User-defined assert. @@ -76,7 +86,7 @@ def check_(condition: bool, message: str = "") -> None: https://bandit.readthedocs.io/en/1.7.5/plugins/b101_assert_used.html """ if not condition: - raise AssertionError(message) + raise exception_cls(message) def parse_ground_fluent(symbol: str) -> Predicate: @@ -99,17 +109,50 @@ def parse_ground_fluent(symbol: str) -> Predicate: return Predicate(symbol) +def _check_does_not_start_with(symbol: str, prefixes: Collection[str]) -> None: + """ + Check if a symbol does not start with a given prefix. + + :param symbol: the symbol + :param prefixes: the prefixes to check + """ + for prefix in prefixes: + check_( + not symbol.startswith(prefix), + f"invalid symbol: symbol '{symbol}' cannot start with {prefix}", + exception_cls=ValueError, + ) + + +def _check_not_in(symbol: str, forbidden_substrings: Collection[str]) -> None: + """ + Check if a string is not in a set of symbols. + + :param symbol: the symbol + :param forbidden_substrings: the set of forbidden substrings + """ + for s in forbidden_substrings: + check_( + s not in symbol, + f"invalid symbol: symbol '{symbol}' contains {s}", + exception_cls=ValueError, + ) + + def validate(symbol: str) -> None: """ Validate a symbol. :param symbol: the symbol """ - # check if the symbol does not start with the 'val__' prefix - if symbol.startswith(_VAL_PREFIX): - raise ValueError( - f"invalid symbol: symbol '{symbol}' cannot start with {_VAL_PREFIX}" - ) + # remove the double quotes + symbol_unquoted = symbol.replace('"', "") + + # check if the symbol does not start with the 'val__' or the 'Y__' prefix + _check_does_not_start_with(symbol_unquoted, [VAL_PREFIX, Y_PREFIX]) + + # check if the symbol does not contain forbidden substrings + _check_not_in(symbol_unquoted, [_LEFT_PAR, _RIGHT_PAR, _AND, _OR, _NOT, _QUOTE]) # check if the symbol is a valid PDDL ground fluent parse_ground_fluent(symbol) diff --git a/plan4past/utils/derived_visitor.py b/plan4past/utils/derived_visitor.py index e0be5143..fb213240 100644 --- a/plan4past/utils/derived_visitor.py +++ b/plan4past/utils/derived_visitor.py @@ -39,7 +39,12 @@ ) from pylogics.utils.to_string import to_string -from plan4past.helpers.utils import add_val_prefix, parse_ground_fluent, replace_symbols +from plan4past.helpers.utils import ( + Y_PREFIX, + add_val_prefix, + parse_ground_fluent, + replace_symbols, +) @singledispatch @@ -132,7 +137,7 @@ def derived_predicates_since(formula: Since) -> Set[DerivedPredicate]: op_or_1 = Predicate(add_val_prefix(replace_symbols(to_string(formula.operands[1])))) op_or_2 = And( Predicate(add_val_prefix(replace_symbols(to_string(formula.operands[0])))), - Predicate(f"Y-{replace_symbols(to_string(formula))}"), + Predicate(f"{Y_PREFIX}{replace_symbols(to_string(formula))}"), ) condition = Or(op_or_1, op_or_2) der_pred_ops = [derived_predicates(op) for op in formula.operands] @@ -146,7 +151,7 @@ def derived_predicates_once(formula: Once) -> Set[DerivedPredicate]: val = Predicate(add_val_prefix(replace_symbols(formula_name))) condition = Or( Predicate(add_val_prefix(replace_symbols(to_string(formula.argument)))), - Predicate(f"Y-{replace_symbols(to_string(formula))}"), + Predicate(f"{Y_PREFIX}{replace_symbols(to_string(formula))}"), ) der_pred_arg = derived_predicates(formula.argument) return {DerivedPredicate(val, condition)}.union(der_pred_arg) diff --git a/plan4past/utils/predicates_visitor.py b/plan4past/utils/predicates_visitor.py index da81c05b..03ac4a07 100644 --- a/plan4past/utils/predicates_visitor.py +++ b/plan4past/utils/predicates_visitor.py @@ -40,7 +40,7 @@ ) from pylogics.utils.to_string import to_string -from plan4past.helpers.utils import replace_symbols +from plan4past.helpers.utils import Y_PREFIX, replace_symbols def predicates_binaryop(formula: _BinaryOp): @@ -113,7 +113,7 @@ def predicates_since(formula: Since) -> Set[Predicate]: tail = Since(*formula.operands[1:]) return predicates(Since(head, tail)) formula_name = replace_symbols(to_string(formula)) - quoted = Predicate(f"Y-{formula_name}") + quoted = Predicate(f"{Y_PREFIX}{formula_name}") subsinces = predicates_binaryop(formula) return {quoted}.union(subsinces) @@ -122,6 +122,6 @@ def predicates_since(formula: Since) -> Set[Predicate]: def predicates_once(formula: Once) -> Set[Predicate]: """Compute predicate for a Once formula.""" formula_name = replace_symbols(to_string(formula)) - quoted = Predicate(f"Y-{formula_name}") + quoted = Predicate(f"{Y_PREFIX}{formula_name}") sub = predicates_unaryop(formula) return sub.union({quoted}) diff --git a/tests/helpers/planutils/downward.py b/tests/helpers/planutils/downward.py index a6ce0172..6ef77122 100644 --- a/tests/helpers/planutils/downward.py +++ b/tests/helpers/planutils/downward.py @@ -68,7 +68,7 @@ def get_planner_cmd( def process_output(self, working_directory: Path, stdout: str) -> PlannerResult: """Process the output of the planner.""" - logger.debug("Processing output of LAMA") + logger.debug("Processing output of Fast-Downward.") # the sas_plan file is in the /root directory sas_file = working_directory / "sas_plan" diff --git a/tests/test_compiler/test_blocksworld_det.py b/tests/test_compiler/test_blocksworld_det.py index a99bb5a9..cdfafe4b 100644 --- a/tests/test_compiler/test_blocksworld_det.py +++ b/tests/test_compiler/test_blocksworld_det.py @@ -35,8 +35,8 @@ class TestBlocksworldDetSimpleSequence(BaseCompilerTest): PATH_TO_DOMAINS_DIR = BLOCKSWORLD_DIR PATH_TO_INSTANCES_DIR = BLOCKSWORLD_DIR - MIN_INSTANCE_ID = 2 - MAX_INSTANCE_ID = 10 + MIN_INSTANCE_ID = 3 + MAX_INSTANCE_ID = 3 def make_formula(self, instance_id: int, domain: Path, problem: Path) -> str: """ diff --git a/tests/test_helpers/test_utils.py b/tests/test_helpers/test_utils.py index 78fad0fa..4620fbca 100644 --- a/tests/test_helpers/test_utils.py +++ b/tests/test_helpers/test_utils.py @@ -33,22 +33,22 @@ def test_val_prefix() -> None: """Test the add_val_prefix function.""" - assert add_val_prefix("Y-foo") == "val__Y-foo" - assert add_val_prefix("Yfoo") == "val__Yfoo" - assert add_val_prefix("foo") == "val__foo" - assert add_val_prefix("Y-foo-bar") == "val__Y-foo-bar" + assert add_val_prefix("Y-foo") == "VAL__Y-foo" + assert add_val_prefix("Yfoo") == "VAL__Yfoo" + assert add_val_prefix("foo") == "VAL__foo" + assert add_val_prefix("Y-foo-bar") == "VAL__Y-foo-bar" def test_remove_before_prefix() -> None: """Test the remove_before_prefix function.""" - assert remove_before_prefix("Y-foo") == "foo" - assert remove_before_prefix("Yfoo") == "foo" + assert remove_before_prefix("Y__foo") == "foo" + assert remove_before_prefix("YLPAR__foo__RPAR") == "foo" assert remove_before_prefix("foo") == "foo" def test_remove_val_prefix() -> None: """Test the remove_val_prefix function.""" - assert remove_val_prefix("val__foo") == "foo" + assert remove_val_prefix("VAL__foo") == "foo" assert remove_val_prefix("foo") == "foo" diff --git a/tests/test_utils/test_derived_visitor.py b/tests/test_utils/test_derived_visitor.py index 6b050df0..7c54d5b2 100644 --- a/tests/test_utils/test_derived_visitor.py +++ b/tests/test_utils/test_derived_visitor.py @@ -101,7 +101,7 @@ def test_derived_predicates_visitor_and(): condition_a = Predicate("a") condition_b = Predicate("b") - val = Predicate(add_val_prefix("a-and-b")) + val = Predicate(add_val_prefix("LPAR__a__RPAR-__AND__-LPAR__b__RPAR")) val_a = Predicate(add_val_prefix("a")) val_b = Predicate(add_val_prefix("b")) @@ -125,7 +125,7 @@ def test_derived_predicates_visitor_or(): condition_a = Predicate("a") condition_b = Predicate("b") - val = Predicate(add_val_prefix("a-or-b")) + val = Predicate(add_val_prefix("LPAR__a__RPAR-__OR__-LPAR__b__RPAR")) val_a = Predicate(add_val_prefix("a")) val_b = Predicate(add_val_prefix("b")) @@ -147,7 +147,7 @@ def test_derived_predicates_visitor_not(): condition_a = Predicate("a") - val = Predicate(add_val_prefix("not-a")) + val = Predicate(add_val_prefix("NOT__LPAR__a__RPAR")) val_a = Predicate(add_val_prefix("a")) condition = Not(val_a) @@ -165,10 +165,10 @@ def test_derived_predicates_visitor_before(): condition_a = Predicate("a") - val = Predicate(add_val_prefix("Ya")) + val = Predicate(add_val_prefix("YLPAR__a__RPAR")) val_a = Predicate(add_val_prefix("a")) - condition = Predicate("Ya") + condition = Predicate("YLPAR__a__RPAR") expected = {DerivedPredicate(val, condition), DerivedPredicate(val_a, condition_a)} @@ -186,10 +186,14 @@ def test_derived_predicates_visitor_since(): val_a = Predicate(add_val_prefix("a")) val_b = Predicate(add_val_prefix("b")) val_c = Predicate(add_val_prefix("c")) - val_a_since_b_since_c = Predicate(add_val_prefix("a-S-b-S-c")) - val_b_since_c = Predicate(add_val_prefix("b-S-c")) - Y_a_since_b_since_c = Predicate("Y-a-S-b-S-c") - Y_b_since_c = Predicate("Y-b-S-c") + val_a_since_b_since_c = Predicate( + add_val_prefix("LPAR__a__RPAR-S-LPAR__LPAR__b__RPAR-S-LPAR__c__RPAR__RPAR") + ) + val_b_since_c = Predicate(add_val_prefix("LPAR__b__RPAR-S-LPAR__c__RPAR")) + Y_a_since_b_since_c = Predicate( + "Y__LPAR__a__RPAR-S-LPAR__LPAR__b__RPAR-S-LPAR__c__RPAR__RPAR" + ) + Y_b_since_c = Predicate("Y__LPAR__b__RPAR-S-LPAR__c__RPAR") condition_a = Predicate("a") condition_b = Predicate("b") @@ -215,8 +219,8 @@ def test_derived_predicates_visitor_once(): once_a = Once(a) val_a = Predicate(add_val_prefix("a")) - val_once_a = Predicate(add_val_prefix("Oa")) - Y_once_a = Predicate("Y-Oa") + val_once_a = Predicate(add_val_prefix("OLPAR__a__RPAR")) + Y_once_a = Predicate("Y__OLPAR__a__RPAR") condition_a = Predicate("a") condition_once_a = Or(val_a, Y_once_a) diff --git a/tests/test_utils/test_predicates_visitor.py b/tests/test_utils/test_predicates_visitor.py index b398570d..9f32884e 100644 --- a/tests/test_utils/test_predicates_visitor.py +++ b/tests/test_utils/test_predicates_visitor.py @@ -84,7 +84,7 @@ def test_predicates_visitor_before(): """Test the predicates visitor for the before formula.""" a = PLTLAtomic("a") Ya = Before(a) - assert predicates(Ya) == {Predicate("Ya")} + assert predicates(Ya) == {Predicate("YLPAR__a__RPAR")} def test_predicates_visitor_since(): @@ -94,8 +94,8 @@ def test_predicates_visitor_since(): c = PLTLAtomic("c") a_since_b_since_c = Since(a, b, c) assert predicates(a_since_b_since_c) == { - Predicate("Y-b-S-c"), - Predicate("Y-a-S-b-S-c"), + Predicate("Y__LPAR__a__RPAR-S-LPAR__LPAR__b__RPAR-S-LPAR__c__RPAR__RPAR"), + Predicate("Y__LPAR__b__RPAR-S-LPAR__c__RPAR"), } @@ -103,4 +103,4 @@ def test_predicates_visitor_once(): """Test the predicates visitor for the once formula.""" a = PLTLAtomic("a") once_a = Once(a) - assert predicates(once_a) == {Predicate("Y-Oa")} + assert predicates(once_a) == {Predicate("Y__OLPAR__a__RPAR")} diff --git a/tests/test_utils/test_val_predicates_visitor.py b/tests/test_utils/test_val_predicates_visitor.py index c28f460c..32440eff 100644 --- a/tests/test_utils/test_val_predicates_visitor.py +++ b/tests/test_utils/test_val_predicates_visitor.py @@ -66,7 +66,7 @@ def test_val_predicates_visitor_and(): a = PLTLAtomic("a") b = PLTLAtomic("b") - val_a_and_b = Predicate(add_val_prefix("a-and-b")) + val_a_and_b = Predicate(add_val_prefix("LPAR__a__RPAR-__AND__-LPAR__b__RPAR")) val_a = Predicate(add_val_prefix(a.name)) val_b = Predicate(add_val_prefix(b.name)) @@ -78,7 +78,7 @@ def test_val_predicates_visitor_or(): a = PLTLAtomic("a") b = PLTLAtomic("b") - val_a_or_b = Predicate(add_val_prefix("a-or-b")) + val_a_or_b = Predicate(add_val_prefix("LPAR__a__RPAR-__OR__-LPAR__b__RPAR")) val_a = Predicate(add_val_prefix(a.name)) val_b = Predicate(add_val_prefix(b.name)) @@ -89,7 +89,7 @@ def test_val_predicates_visitor_not(): """Test the val predicates visitor for the not formula.""" a = PLTLAtomic("a") - val_not_a = Predicate(add_val_prefix("not-a")) + val_not_a = Predicate(add_val_prefix("NOT__LPAR__a__RPAR")) val_a = Predicate(add_val_prefix(a.name)) assert val_predicates(~a) == {val_not_a, val_a} @@ -100,7 +100,7 @@ def test_val_predicates_visitor_before(): a = PLTLAtomic("a") before_a = Before(a) - val_before_a = Predicate(add_val_prefix("Ya")) + val_before_a = Predicate(add_val_prefix("YLPAR__a__RPAR")) val_a = Predicate(add_val_prefix(a.name)) assert val_predicates(before_a) == {val_before_a, val_a} @@ -113,8 +113,10 @@ def test_val_predicates_visitor_since(): c = PLTLAtomic("c") a_since_b_since_c = Since(a, b, c) - val_a_since_b_since_c = Predicate(add_val_prefix("a-S-b-S-c")) - val_b_since_c = Predicate(add_val_prefix("b-S-c")) + val_a_since_b_since_c = Predicate( + add_val_prefix("LPAR__a__RPAR-S-LPAR__LPAR__b__RPAR-S-LPAR__c__RPAR__RPAR") + ) + val_b_since_c = Predicate(add_val_prefix("LPAR__b__RPAR-S-LPAR__c__RPAR")) val_a = Predicate(add_val_prefix(a.name)) val_b = Predicate(add_val_prefix(b.name)) val_c = Predicate(add_val_prefix(c.name)) @@ -133,7 +135,7 @@ def test_val_predicates_visitor_once(): a = PLTLAtomic("a") once_a = Once(a) - val_once_a = Predicate(add_val_prefix("Oa")) + val_once_a = Predicate(add_val_prefix("OLPAR__a__RPAR")) val_a = Predicate(add_val_prefix(a.name)) assert val_predicates(once_a) == {val_once_a, val_a}