Commit 159f678c authored by Arthur Bit-Monnot's avatar Arthur Bit-Monnot

More closely match the PDDL semantics.

parent d92483e3
......@@ -103,7 +103,7 @@ class Z3PartialSolver[X](_ast: RootedLazyTree[X, Total, cats.Id]) extends Partia
assert(model == null, "Z3 only support extraction of a single solution")
deadline match {
case Some(dl) if dl.isOverdue => return None // deadline passed, to not attempt to solve
case Some(dl) if dl.isOverdue => return None // deadline passed, do not attempt to solve
case Some(t) =>
val params = ctx.mkParams()
params.add("timeout", t.timeLeft.toMillis.toInt)
......
......@@ -142,13 +142,13 @@ package object core {
lazy val start: LocalVar = content
.collectFirst {
case LocalVarDeclaration(tp @ LocalVar(Id(`scope`, "start"), predef.Time)) => tp
case LocalVarDeclaration(tp @ LocalVar(Id(`scope`, predef.StartSym), predef.Time)) => tp
}
.getOrElse(sys.error("No start timepoint in this action"))
lazy val end: LocalVar = content
.collectFirst {
case LocalVarDeclaration(tp @ LocalVar(Id(`scope`, "end"), predef.Time)) => tp
case LocalVarDeclaration(tp @ LocalVar(Id(`scope`, predef.EndSym), predef.Time)) => tp
}
.getOrElse(sys.error("No end timepoint in this action"))
}
......
......@@ -105,21 +105,49 @@ object ActionFactory {
def add(t: TemporalQualifier, e: TimedAssertion): Unit = {
mod = mod + TemporallyQualifiedAssertion(t, e)
}
def regroup(qual: TQual, cond: TimedEqualAssertion, eff: TimedAssignmentAssertion): Ass = {
assert(cond.fluent == eff.fluent)
Ass(qual,
TimedTransitionAssertion(cond.fluent,
cond.right,
eff.to,
Some(act.base),
act.base.scope.makeNewId()))
}
val merged: Iterable[Ass] = act.assertions
.groupBy(a => (a.qual, a.ass.fluent))
.values
.map(_.toList)
.map({
case e :: Nil => e
case Ass(t, cond: TimedEqualAssertion) :: Ass(t2, eff: TimedAssignmentAssertion) :: Nil =>
assert(t == t2 && cond.fluent == eff.fluent)
regroup(t, cond, eff)
case Ass(t2, eff: TimedAssignmentAssertion) :: Ass(t, cond: TimedEqualAssertion) :: Nil =>
assert(t == t2 && cond.fluent == eff.fluent)
regroup(t, cond, eff)
})
val afterStart = BinaryExprTree(operators.Add, start, predef.Epsilon)
val afterEnd = BinaryExprTree(operators.Add, end, predef.Epsilon)
import TQual._
for(ass <- act.assertions) ass match {
for(ass <- merged) ass match {
case Ass(Start, e: TimedEqualAssertion) =>
add(Equals(ClosedInterval(start, start)), e)
add(Equals(ClosedInterval(start, afterStart)), e)
case Ass(End, e: TimedEqualAssertion) =>
add(Equals(ClosedInterval(end, end)), e)
add(Equals(ClosedInterval(end, afterEnd)), e)
case Ass(All, e: TimedEqualAssertion) =>
add(Equals(ClosedInterval(start, end)), e)
add(Equals(ClosedInterval(start, end)), e) //TODO: probably does not match pddl semantics
case Ass(Start, e: TimedAssignmentAssertion) =>
add(Equals(LeftOpenInterval(start, BinaryExprTree(operators.Add, start, predef.Epsilon))),
e)
add(Equals(LeftOpenInterval(start, afterStart)), e)
case Ass(End, e: TimedAssignmentAssertion) =>
add(Equals(LeftOpenInterval(end, BinaryExprTree(operators.Add, end, predef.Epsilon))), e)
case _ => unexpected
add(Equals(LeftOpenInterval(end, afterEnd)), e)
case Ass(Start, e: TimedTransitionAssertion) =>
add(Equals(ClosedInterval(start, afterStart)), e)
case Ass(End, e: TimedTransitionAssertion) =>
add(Equals(ClosedInterval(end, afterEnd)), e)
}
mod
}
......
......@@ -26,10 +26,11 @@ class Parser(opt: Options) {
def parse(domain: File, problem: File): Try[CoreModel] = {
parseToFull(domain, problem).flatMap { m =>
val coreM = FullToCore.trans(m)
if(opt.optimize)
new ActionRewrite(opt).optimize(m).map(FullToCore.trans(_))
new ActionRewrite(opt).optimize(coreM)
else
Try(FullToCore.trans(m))
Success(coreM)
}
}
}
package dahu.planning.pddl.parser.optim
import dahu.planning.model.common.Interval.OpenOnRight
import dahu.planning.model.common.Interval.{ClosedOnLeft, ClosedOnRight, OpenOnLeft, OpenOnRight}
import dahu.planning.model.common._
import dahu.planning.model.full._
import dahu.planning.model.core._
import dahu.planning.pddl.parser.{Options, PddlPredef}
import spire.syntax.cfor
......@@ -11,8 +11,8 @@ import scala.collection.mutable
import scala.util.Try
class ActionRewrite(options: Options) {
def optimize(model: Model)(implicit predef: Predef): Try[Model] = Try {
implicit val ctx: Ctx = model
def optimize(model: CoreModel)(implicit predef: Predef): Try[CoreModel] = Try {
// implicit val ctx: Ctx = model
val f: InModuleBlock => InModuleBlock = {
case e: ActionTemplate => opt(e)
case x => x
......@@ -20,71 +20,99 @@ class ActionRewrite(options: Options) {
model.map(f)
}
def opt(a: ActionTemplate)(implicit predef: Predef, ctx: Ctx): ActionTemplate = {
def opt(a: ActionTemplate)(implicit predef: Predef): ActionTemplate = {
def println(str: Any): Unit = Predef.println(str.toString.replaceAll(a.name + "\\.", ""))
val timelines = a.store.blocks
.collect { case x: TemporallyQualifiedAssertion => x }
val timelines = a.content
.collect { case x: TimedAssertion => x }
.map(assertionToTimeline)
.sortBy(_.toString)
if(options.lint) {
val regrouped = regroup(timelines).sortBy(_.toString)
// if(options.lint) {
val regrouped = regroup(timelines).sortBy(_.toString)
// timelines.foreach(println)
// println(" ============ ")
regrouped.foreach(println)
println("")
regrouped.map(encode).foreach(x => println(x.mkString(" ------ ")))
println("")
}
// regrouped.foreach(println)
// println("")
// regrouped.map(encode).foreach(x => println(x.mkString(" ------ ")))
println("")
// println("GROUPED: ")
// regrouped
// .groupBy(_.fluent)
// .values
// .filter(_.size > 1)
// .foreach(x => println(x.mkString(" ---------> ")))
val merged = removeDiscontinuitiesUnsafe(regrouped, a.start, a.end)
// merged.flatMap(encode).foreach(println)
// }
val content = a.content.filterNot(_.isInstanceOf[TimedAssertion]) ++ merged.flatMap(encode)
// println(xx)
a
ActionTemplate(a.scope, content)
// a
}
def removeDiscontinuitiesUnsafe(timelines: Seq[Timeline],
start: StaticExpr,
end: StaticExpr): Seq[Timeline] = {
val ordering: (StaticExpr, StaticExpr) => PartialOrdering = {
start: Expr,
end: Expr): Seq[Timeline] = {
val ordering: (Expr, Expr) => PartialOrdering = {
case (l, r) if l == start && r == end => After
case (l, r) if r == start && l == end => Before
case _ => Unordered
}
def merge(before: Timeline, after: Timeline): Timeline = {
assert(before.fluent == after.fluent)
val header = before.toks.dropRight(1)
val footer = after.toks.drop(1)
val l = before.toks.last
val r = after.toks.head
val middleToks = (l, r) match {
case (Is(itv: OpenOnRight, v), Undef(itv2: OpenOnRight)) =>
Is(itv, v) :: Undef(RightOpenInterval(itv.end, itv2.end)) :: Nil
case (Is(itv: ClosedOnRight, v), Undef(itv2: OpenOnRight)) =>
Is(itv, v) :: Undef(OpenInterval(itv.end, itv2.end)) :: Nil
case (lhs @ Becomes(t, v), rhs @ Undef(itv: OpenOnLeft)) =>
lhs :: Is(LeftOpenInterval(t, itv.start), v) :: rhs :: Nil
case (lhs @ Becomes(t, v), rhs @ Undef(itv: ClosedOnLeft)) =>
lhs :: Is(OpenInterval(t, itv.start), v) :: rhs :: Nil
}
Timeline(before.fluent, header ++ middleToks ++ footer: _*)
}
timelines.groupBy(_.fluent).values.toSeq.map {
case Seq(tl) => tl
case Seq(tl1, tl2) =>
println(s"warning: merging two discontinuous timelines: $tl1 ----- $tl2")
tl1.order(tl2, ordering) match {
case After => ???
case Before => ???
case After => merge(tl1, tl2)
case Before => merge(tl2, tl1)
case Unordered => ???
}
}
}
private def tqa(itv: Interval[StaticExpr],
assertion: TimedAssertion): TemporallyQualifiedAssertion =
TemporallyQualifiedAssertion(Equals(itv), assertion)
// private def tqa(itv: Interval[Expr],
// assertion: TimedAssertion): TemporallyQualifiedAssertion =
// TemporallyQualifiedAssertion(Equals(itv), assertion)
def encode(tl: Timeline)(implicit predef: Predef, ctx: Ctx): Seq[TemporallyQualifiedAssertion] = {
def encode(tl: Timeline)(implicit predef: Predef): Seq[TimedAssertion] = {
val fluent = tl.fluent
def id(): Id = ctx.scope.makeNewId()
def go(toks: List[Token]): List[TemporallyQualifiedAssertion] = toks match {
// def id(): Id = ctx.scope.makeNewId()
def go(toks: List[Token]): List[TimedAssertion] = toks match {
case Is(Point(a), from) :: Undef(_) :: Becomes(b, to) :: rest =>
tqa(
ClosedInterval(a, b),
TimedTransitionAssertion(fluent, from, to, Some(ctx), id())
) :: go(rest)
TimedTransitionAssertion(ClosedInterval(a, b), fluent, from, to) :: go(rest)
case Undef(itv) :: Becomes(a, v) :: rest =>
if(itv.isLeftOpen)
tqa(LeftOpenInterval(itv.start, a),
TimedAssignmentAssertion(tl.fluent, v, Some(ctx), id())) :: go(rest)
TimedAssignmentAssertion(LeftOpenInterval(itv.start, a), tl.fluent, v) :: go(rest)
else
tqa(ClosedInterval(itv.start, a), TimedAssignmentAssertion(tl.fluent, v, Some(ctx), id())) :: go(
rest)
TimedAssignmentAssertion(ClosedInterval(itv.start, a), tl.fluent, v) :: go(rest)
case Becomes(a, v) :: rest =>
tqa(Point(a), TimedAssignmentAssertion(tl.fluent, v, Some(ctx), id())) :: go(rest)
TimedAssignmentAssertion(Point(a), tl.fluent, v) :: go(rest)
case Is(itv, v) :: rest =>
tqa(itv, TimedEqualAssertion(tl.fluent, v, Some(ctx), id())) :: go(rest)
TimedEqualAssertion(itv, tl.fluent, v) :: go(rest)
case Nil => Nil
}
go(tl.toks.toList)
......@@ -112,11 +140,11 @@ class ActionRewrite(options: Options) {
}
}
def assertionToTimeline(e: TemporallyQualifiedAssertion): Timeline = e match {
case TemporallyQualifiedAssertion(Equals(itv), TimedEqualAssertion(f, v, _, _)) =>
def assertionToTimeline(e: TimedAssertion): Timeline = e match {
case TimedEqualAssertion(itv, f, v) =>
Timeline(f, Is(itv, v))
case TemporallyQualifiedAssertion(Equals(itv), TimedAssignmentAssertion(f, v, _, _)) =>
case TimedAssignmentAssertion(itv, f, v) =>
itv match {
case Point(t) => Timeline(f, Becomes(t, v))
case ClosedInterval(s, e) =>
......@@ -126,7 +154,7 @@ class ActionRewrite(options: Options) {
case _ => ???
}
case TemporallyQualifiedAssertion(Equals(itv), TimedTransitionAssertion(f, from, to, _, _)) =>
case TimedTransitionAssertion(itv, f, from, to) =>
itv match {
case Point(_) => ???
case ClosedInterval(s, e) =>
......@@ -152,18 +180,18 @@ object Point {
sealed trait AfterIs
sealed trait Token {
def itv: Interval[StaticExpr]
def itv: Interval[Expr]
def rightBefore(next: Token): Boolean =
itv.end == next.itv.start && itv.isRightOpen != next.itv.isLeftOpen
}
case class Undef(itv: Interval[StaticExpr] with OpenOnRight) extends Token with AfterIs
case class Becomes(at: StaticExpr, v: StaticExpr) extends Token with AfterIs {
def itv: Interval[StaticExpr] = Point(at)
case class Undef(itv: Interval[Expr] with OpenOnRight) extends Token with AfterIs
case class Becomes(at: Expr, v: Expr) extends Token with AfterIs {
def itv: Interval[Expr] = Point(at)
}
case class Is(itv: Interval[StaticExpr], v: StaticExpr) extends Token
case class Is(itv: Interval[Expr], v: Expr) extends Token
class Timeline(val fluent: TimedExpr, val toks: Seq[Token]) {
class Timeline(val fluent: Fluent, val toks: Seq[Token]) {
// timeline must be continuous
require(toks.nonEmpty)
require((1 until toks.size).forall(i => toks(i - 1).rightBefore(toks(i))))
......@@ -179,7 +207,7 @@ class Timeline(val fluent: TimedExpr, val toks: Seq[Token]) {
}
def order(tl: Timeline, tpOrder: (StaticExpr, StaticExpr) => PartialOrdering): PartialOrdering = {
def order(tl: Timeline, tpOrder: (Expr, Expr) => PartialOrdering): PartialOrdering = {
if(fluent != tl.fluent) Unordered
else if(toks.last.rightBefore(tl.toks.head)) RightAfter
else if(tl.toks.last.rightBefore(toks.head)) RightBefore
......@@ -196,8 +224,8 @@ class Timeline(val fluent: TimedExpr, val toks: Seq[Token]) {
}
}
object Timeline {
def apply(fluent: TimedExpr, toks: Token*): Timeline = new Timeline(fluent, toks.toVector)
def unapply(tl: Timeline): Option[(TimedExpr, Seq[Token])] = Some((tl.fluent, tl.toks))
def apply(fluent: Fluent, toks: Token*): Timeline = new Timeline(fluent, toks.toVector)
def unapply(tl: Timeline): Option[(Fluent, Seq[Token])] = Some((tl.fluent, tl.toks))
}
sealed trait PartialOrdering
......
......@@ -2,6 +2,7 @@ package dahu.planning.pddl.planner
import java.io.File
import dahu.planning.model.core.ActionTemplate
import dahu.planning.pddl.parser._
import dahu.planning.planner._
import dahu.utils.Vec
......@@ -81,7 +82,17 @@ object Main extends App {
val parser = new Parser(pddlOptions)
implicit val predef: PddlPredef = parser.predef
parser.parse(domain, problem)
parser.parse(domain, problem) match {
case Success(x) =>
x.foreach {
case a @ ActionTemplate(_, content) =>
println()
println(a)
content.distinct.foreach(x => println(" " + x))
case _ =>
}
case Failure(e) => throw e
}
}
type Plan = String
......
......@@ -5,15 +5,31 @@ import java.io.File
import ammonite.ops._
import dahu.planning.pddl.parser.PddlPredef
import dahu.utils.debug._
import scala.util.{Failure, Success, Try}
object Validator {
def validate(domain: File, problem: File, plan: PddlPlan)(implicit predef: PddlPredef): Boolean = {
def validate(domain: File, problem: File, plan: PddlPlan)(
implicit predef: PddlPredef): Boolean = {
val tolerance: Double = 1.0 / predef.discretization.toDouble
val out = File.createTempFile("plan", "")
write.over(Path(out), plan.format)
val ret = %%('validate, "-t", tolerance, domain.getAbsolutePath, problem.getAbsolutePath, out.getAbsolutePath)(pwd)
Try(
%%('validate,
"-v",
"-t",
tolerance,
domain.getAbsolutePath,
problem.getAbsolutePath,
out.getAbsolutePath)(pwd)) match {
case Success(_) =>
info("Plan validated.")
case Failure(e: ShelloutException) =>
error("Invalid plan:")
println(e)
}
println(ret)
true
}
......
......@@ -155,7 +155,7 @@ final class Vec[@sp A](private val elems: Array[A])(implicit val ct: ClassTag[A]
val n = j - i
val arr = new Array[A](n)
System.arraycopy(elems, i, arr, 0, n)
new Vec(arr)
Vec.unsafe(arr)
}
/**
......@@ -173,7 +173,7 @@ final class Vec[@sp A](private val elems: Array[A])(implicit val ct: ClassTag[A]
i += 1
j -= 1
}
new Vec(arr)
Vec.unsafe(arr)
}
/**
......
......@@ -67,6 +67,7 @@ object debug {
}
@inline final def error(msg: => String): Unit = println("error: " + msg)
@inline final def warning(msg: => String): Unit = if(LOG_LEVEL >= 1) println("warning: " + msg)
@inline final def info(msg: => String): Unit =
if(LOG_LEVEL >= 3) {
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment