Core definitions for the STRIPS formalism

We define some basic definitions of the STRIPS formalism for automated planning (TODO : cite). This file only contains the definitions that belong to the trusted core of the project, i.e. definitions that are needed to define planning problems themselves and unsolvability of planning problems. Additional definitions can be found in Validator.PlanningTask.Basic.

Implementation Notes

Some definitions in this file have two version:

• an primed version which uses a representation that is efficient for representing instances at run-time, and
• an unprimed version which is more suited for theoretical results (usually using Finset).

Exceptions are Action and STRIPS which can be used for both purposes.

Sets of variables

Variables have type Fin n, and sets of variables therefore have type Finset(Fin n). At runtime we use an Array instead of Finset.

@[reducible, inline]

abbrev Validator.VarSet (n : ℕ) : Type

Equations

• Validator.VarSet n = Set (Fin n)

@[reducible, inline]

abbrev Validator.VarSet' (n : ℕ) : Type

Equations

• Validator.VarSet' n = { vars : List (Fin n) // vars.SortedLT }

def Validator.convertVarSet {n : ℕ} (V : VarSet' n) : VarSet n

Equations

• Validator.convertVarSet V = ↑(↑V).toFinset

States and sets of states

From a theoretical perspective states are just set of variables, but at runtime they are represented by a vector with boolean values to indicate which variables are in the set.

TODO : sets of states at runtime

@[reducible, inline]

abbrev Validator.State (n : ℕ) : Type

Equations

• Validator.State n = Set (Fin n)

@[reducible, inline]

abbrev Validator.State' (n : ℕ) : Type

Equations

• Validator.State' n = BitVec n

@[reducible, inline]

abbrev Validator.States (n : ℕ) : Type

Equations

• Validator.States n = Set (Validator.State n)

def Validator.convertState {n : ℕ} (s' : State' n) : State n

Equations

• Validator.convertState s' = {i : Fin n | s'[i] = true}

Actions and sets of actions

structure Validator.Action (n : ℕ) : Type

Actions in the STRIPS formalism

• name : String

  The name of the action.

• pre' : VarSet' n

  The preconditions of the action. See Action.pre for the version using VarSet.

• add' : VarSet' n

  The adding effects of the action. See Action.add for the version using VarSet.

• del' : VarSet' n

  The deleting effects of the action. See Action.pre for the version using VarSet.

• cost : ℕ

  The cost of the action.

def Validator.instReprAction.repr {n✝ : ℕ} : Action n✝ → ℕ → Std.Format

Equations

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

instance Validator.instReprAction {n✝ : ℕ} : Repr (Action n✝)

Equations

• Validator.instReprAction = { reprPrec := Validator.instReprAction.repr }

instance Validator.instDecidableEqAction {n✝ : ℕ} : DecidableEq (Action n✝)

Equations

• Validator.instDecidableEqAction = Validator.instDecidableEqAction.decEq

def Validator.instDecidableEqAction.decEq {n✝ : ℕ} (x✝ x✝¹ : Action n✝) : Decidable (x✝ = x✝¹)

Equations

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

def Validator.Action.pre {n : ℕ} (a : Action n) : VarSet n

Equations

• a.pre = Validator.convertVarSet a.pre'

def Validator.Action.add {n : ℕ} (a : Action n) : VarSet n

Equations

• a.add = Validator.convertVarSet a.add'

def Validator.Action.del {n : ℕ} (a : Action n) : VarSet n

Equations

• a.del = Validator.convertVarSet a.del'

@[reducible, inline]

abbrev Validator.Actions (n : ℕ) : Type

Equations

• Validator.Actions n = Set (Validator.Action n)

@[reducible, inline]

abbrev Validator.Actions' (n : ℕ) : Type

Equations

• Validator.Actions' n = List (Validator.Action n)

Applicability and successor states

@[reducible, inline]

abbrev Validator.Applicable {n : ℕ} (s : State n) (a : Action n) : Prop

An action is applicable in a state if all its preconditions are true in the state.

Equations

• Validator.Applicable s a = (a.pre ⊆ s)

@[reducible, inline]

abbrev Validator.Successor {n : ℕ} (a : Action n) (s s' : State n) : Prop

If an action a is applicable in a state s, then s[a] := (s \ a.del) ∪ a.add is the successor of s.

Equations

• Validator.Successor a s s' = (Validator.Applicable s a ∧ s' = s \ a.del ∪ a.add)

STRIPS planning problems

structure Validator.STRIPS (n : ℕ) : Type

A planning problem in the STRIPS formalism. The variables of the planning task are all elements of Fin n.

• varNames : Vector String n

  The names of the variables.

• actions' : Actions' n

  The actions of the planning problem. See STRIPS.actions for the version using Actions.

• init' : State' n

  The initial state of the planning problem. See STRIPS.init for the version using State.

• goal' : VarSet' n

  The goal of the planning problem, indicating which variables need to be true in a goal state. See also GoalState and STRIPS.goal_states in Validator.PlanningTask.Basic.

def Validator.instReprSTRIPS.repr {n✝ : ℕ} : STRIPS n✝ → ℕ → Std.Format

Equations

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

instance Validator.instReprSTRIPS {n✝ : ℕ} : Repr (STRIPS n✝)

Equations

• Validator.instReprSTRIPS = { reprPrec := Validator.instReprSTRIPS.repr }

def Validator.STRIPS.actions {n : ℕ} (pt : STRIPS n) : Actions n

Equations

• pt.actions = ↑(List.toFinset pt.actions')

def Validator.STRIPS.init {n : ℕ} (pt : STRIPS n) : State n

Equations

• pt.init = Validator.convertState pt.init'

def Validator.STRIPS.GoalState {n : ℕ} (pt : STRIPS n) (s : State n) : Prop

Equations

• pt.GoalState s = (Validator.convertVarSet pt.goal' ⊆ s)

Paths in state space and plans

inductive Validator.Path {n : ℕ} (pt : STRIPS n) : State n → State n → Type

Given a STRIPS planning task pt, Path s1 s2 is a path form the state s1 to the state s2 in the state space of pt.

• empty {n : ℕ} {pt : STRIPS n} (s : State n) : Path pt s s

  The empty path consisting of a single node s.

• cons {n : ℕ} {pt : STRIPS n} (a : Action n) {s1 : State n} (s2 : State n) {s3 : State n} (ha : a ∈ pt.actions) (succ : Successor a s1 s2) (π : Path pt s2 s3) : Path pt s1 s3

  The path consisting of the node s, and the path π, where s[a] is the first node of π.

structure Validator.Plan {n : ℕ} (pt : STRIPS n) (s : State n) : Type

A plan for a state s for a planning task pt is a path from s to a goal state of pt.

• last : State n

  The goal state in pt.

• path : Path pt s self.last

  The path from s to the goal state.

• goal : pt.GoalState self.last

  The proof that last is a goal state.

Unsolvability

@[reducible, inline]

abbrev Validator.UnsolvableState {n : ℕ} (pt : STRIPS n) (s : State n) : Prop

A state is unsolvable if there is no plan for that state.

Equations

• Validator.UnsolvableState pt s = IsEmpty (Validator.Plan pt s)

@[reducible, inline]

abbrev Validator.Unsolvable {n : ℕ} (pt : STRIPS n) : Prop

A planning task is unsolvable if the initial state is unsolvable.

Equations

• Validator.Unsolvable pt = Validator.UnsolvableState pt pt.init