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

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 invocation
$ ./planning2S5 d.pddl p.pddl -t 5
# 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

Links used for this work