The planning-to-s5 translator
planning2S5: translating PDDL instances into Modal Logic S5 formulae
planning2S5 is a translator associating with an planning instance with uncertainties encoded in PDDL (Planning Domain Definition Language) and a given horizon an output which consists of a modal logic S5 formula. The valid plans for the input planning instance with uncertainties correspond to the models of the corresponding output modal logic S5 formula, projected onto the action variables.
Ressources for the planning2S5 translator
- The runtime code of planning2S5 GNU/Linux operating system
- The source code in C++ will soon be available
How to use planning2S5
Given a PDDL instance of an planning problem with uncertainties,
represented by a domain file d.pddl
, a problem file p.pddl
, and a horizon
(5 in the example developed below), planning2S5 can be run as follows:
Everyline starting with a #
is a log and is written on the standard output.
The instance of modal logic S5 written in InToHyLo is written on the error output though
# planning2S5 version 0.1
# Copyright 2017, CRIL - Artois University, France
# Based on pddl2cnf, CRIL - Artois University, France
# Horizon: 5
# Parsing .........................
# Get domain content ..............
# Parse domain name ...............
# Parse domain fluents ............
# Parse domain actions ............
# Get instance content ............
# Check domain name ...............
# Parse objects ...................
# Parse init constraints ..........
# Parse goal constraints ..........
# Propositionalizing ..............
# Set actions .....................
# Index * predicate1(x1,0) * 1
# Index * predicate1(x1,1) * 2
# Index * predicate1(x1,2) * 3
# Index * predicate1(x1,3) * 4
# Index * predicate1(x1,4) * 5
# Index * predicate1(x1,5) * 6
# Index * predicate2(x1,0) * 7
# Index * ................ * N
# Set fluents .....................
# Set init clauses ................
# Propositionalize ................ predicat1(?x:)
# Propositionalize ................ predicat2(?x:)
# Propositionalize ................ predicat3(?x:)
# Propositionalize ................ predicat4(?x:)
# Propositionalize ................ ..............
# Propositionalize ................ predicatN(?x:)
# Set goal clauses ................
# Set preconditions clauses .......
# Set effect clauses ..............
# Set mutex clauses ...............
# Set frame clauses ...............
# Encode actions ..................
# Encode initial fluents ..........
# Encode goal fluents .............
# Encode theory ...................
# Init encoded ................
# Goal encoded ................
# Preconditions encoded .......
# Effects encoded .............
# Frame encoded ...............
# Mutex encoded ...............
# Write intohylo file .............
# goal & initial fluents without symmetries
begin
intohylo-instance
end
# index_actions 1 2 3 4 5 6 ... N 0
The translator writes on the two output stream
standard output
contains log information (like the relation between the propositional variables and their PDDL equivalent)error output
contains the formula itself encoded in modal logic S5 and written in the InToHyLo format
Links used for this work
- The modal logic S5 solver S52SAT: http://www.cril.univ-artois.fr/~montmirail/s52SAT/
- The PDDL instances for classical planning with uncertainties: https://fai.cs.uni-saarland.de/hoffmann/ff/cff-tests.tgz
- The MaxSAT solvers used:
- MaxHS-b : http://www.maxhs.org/
- MSCG-2015b: https://core.di.fc.ul.pt/~aign/soft/mscg15b-linux-x86-64
- MSUNCORE: http://logos.ucd.ie/wiki/doku.php?id=msuncore
- The MCS-extractor LBX used: http://logos.ucd.ie/web/doku.php?id=lbx