Parser for STRIPS Planning Tasks

This file defines a parser for STRIPS planning tasks in the format used by the certificate checker helve, see https://github.com/salome-eriksson/helve.

def STRIPS.readPlanningTask (path : System.FilePath) : IO ((n : ℕ) × PlanningTask n)

Parse a STRIPS planning problem from the given file. The file is expected to have the following format:

begin_atoms: <#atoms>
<atom 0>
<atom 1>
. . . (names of all atoms, one on each line)
end_atoms
begin_init
<initital state atom index 0>
<initital state atom index 1>
. . . (indexes of atoms that are true in initial state, one on each line)
end_init
begin_goal
<goal atom index 0>
<goal atom index 1>
. . . (indexes of atoms that are true in goal, one on each line)
end_goal
begin_actions: <#actions>
begin_action
<action_name>
cost: <action_cost>
PRE: <precondition atom index 0>
ADD: <added atom index 0>
DEL: <deleted atom index 0>
. . . (more PRE, ADD and DEL in any order, one on each line)
end_action
. . . (more actions)
end_actions

Equations

• One or more equations did not get rendered due to their size.