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.

Sets of variables

Variables have type Fin n. Sets of variables are represented by a bitvector of length n.

@[reducible, inline]

abbrev Validator.VarSet (n : ℕ) : Type

Equations

• Validator.VarSet n = BitVec n

@[implicit_reducible]

instance Validator.VarSet.instEmptyCollection {n : ℕ} : EmptyCollection (VarSet n)

Equations

• Validator.VarSet.instEmptyCollection = { emptyCollection := BitVec.zero n }

def Validator.VarSet.insert {n : ℕ} (i : Fin n) (V : VarSet n) : VarSet n

Equations

• Validator.VarSet.insert i V = V ||| BitVec.twoPow n ↑i

def Validator.VarSet.ofList {n : ℕ} (l : List (Fin n)) : VarSet n

Equations

• Validator.VarSet.ofList l = List.foldr Validator.VarSet.insert ∅ l

@[implicit_reducible]

instance Validator.VarSet.instSetLikeFin {n : ℕ} : SetLike (VarSet n) (Fin n)

Equations

• Validator.VarSet.instSetLikeFin = { coe := fun (V : Validator.VarSet n) => {i : Fin n | V[i] = true}, coe_injective := ⋯ }

States and sets of states

@[reducible, inline]

abbrev Validator.State (n : ℕ) : Type

A state is a set of variables, containing all variables that are true.

Equations

• Validator.State n = Set (Fin n)

@[reducible, inline]

abbrev Validator.States (n : ℕ) : Type

Equations

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

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.

• add : VarSet n

  The adding effects of the action.

• del : VarSet n

  The deleting effects of the action.

• 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.

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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.

@[reducible, inline]

abbrev Validator.Actions (n : ℕ) : Type

Equations

• Validator.Actions n = Set (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. Note that most fields have two version:

• an primed version which uses a representation that is efficient at run-time, and
• an unprimed version which is more suited for theoretical results

• varNames : Vector String n

  The names of the variables.

• actions' : List (Action n)

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

• init' : VarSet 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.

@[implicit_reducible]

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 = ↑pt.actions'.toFinset

@[simp]

theorem Validator.STRIPS.mem_action' {n : ℕ} {pt : STRIPS n} {a : Action n} : a ∈ pt.actions' ↔ a ∈ pt.actions

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

Equations

• pt.init = ↑pt.init'

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

Equations

• pt.GoalState s = (↑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