Commit d92483e3 authored by Arthur Bit-Monnot's avatar Arthur Bit-Monnot

Initial work on linter for PDDL

parent 6fc323ff
......@@ -24,6 +24,11 @@ sealed abstract class Interval[A] {
}
}
object Interval {
sealed trait OpenOnLeft { self: Interval[_] =>}
sealed trait ClosedOnLeft { self: Interval[_] =>}
sealed trait OpenOnRight { self: Interval[_] =>}
sealed trait ClosedOnRight { self: Interval[_] =>}
def point[A](pt: A): Interval[A] = ClosedInterval(pt, pt)
implicit def orderedInstance[A](implicit O: Orderable[A]): Orderable.Aux[Interval[A], O.Bool] =
......@@ -40,26 +45,27 @@ object Interval {
O.lt(a.end, b.start)
}
}
import Interval._
case class ClosedInterval[A](start: A, end: A) extends Interval[A] {
case class ClosedInterval[A](start: A, end: A) extends Interval[A] with ClosedOnLeft with ClosedOnRight {
override def toString: String = s"[$start, $end]"
override def isLeftOpen: Boolean = false
override def isRightOpen: Boolean = false
}
case class LeftOpenInterval[A](start: A, end: A) extends Interval[A] {
case class LeftOpenInterval[A](start: A, end: A) extends Interval[A] with OpenOnLeft with ClosedOnRight {
override def toString: String = s"]$start, $end]"
override def isLeftOpen: Boolean = true
override def isRightOpen: Boolean = false
}
case class RightOpenInterval[A](start: A, end: A) extends Interval[A] {
case class RightOpenInterval[A](start: A, end: A) extends Interval[A] with ClosedOnLeft with OpenOnRight {
override def toString: String = s"[$start, $end["
override def isLeftOpen: Boolean = false
override def isRightOpen: Boolean = true
}
case class OpenInterval[A](start: A, end: A) extends Interval[A] {
case class OpenInterval[A](start: A, end: A) extends Interval[A] with OpenOnLeft with OpenOnRight {
override def toString: String = s"]$start, $end["
override def isLeftOpen: Boolean = true
override def isRightOpen: Boolean = true
......
......@@ -47,7 +47,10 @@ class ActionFactory(actionName: String, parent: Resolver, model: Model) extends
rec(
TemporallyQualifiedAssertion(
Equals(ClosedInterval(start, start)),
TimedEqualAssertion(resolver.getTranslator(f).fluent(f, args, resolver), duration, Some(context), model.scope.makeNewId())
TimedEqualAssertion(resolver.getTranslator(f).fluent(f, args, resolver),
duration,
Some(context),
model.scope.makeNewId())
)
)
case x =>
......@@ -67,15 +70,15 @@ class ActionFactory(actionName: String, parent: Resolver, model: Model) extends
}
def assertions(conds: Exp, effs: Exp): Seq[Ass] = {
def getPre(pre: Exp): Seq[Ass] = pre match {
case ast.And(subs) => subs.flatMap(getPre)
case ast.And(subs) => subs.flatMap(getPre)
case ast.AtStart(e) => Ass(TQual.Start, asCondAss(e)) :: Nil
case ast.AtEnd(e) => Ass(TQual.End, asCondAss(e)) :: Nil
case ast.AtEnd(e) => Ass(TQual.End, asCondAss(e)) :: Nil
case ast.OverAll(e) => Ass(TQual.All, asCondAss(e)) :: Nil
}
def getEff(pre: Exp): Seq[Ass] = pre match {
case ast.And(subs) => subs.flatMap(getEff)
case ast.And(subs) => subs.flatMap(getEff)
case ast.AtStart(e) => Ass(TQual.Start, asEffectAss(e)) :: Nil
case ast.AtEnd(e) => Ass(TQual.End, asEffectAss(e)) :: Nil
case ast.AtEnd(e) => Ass(TQual.End, asEffectAss(e)) :: Nil
case ast.OverAll(e) => Ass(TQual.All, asEffectAss(e)) :: Nil
}
getPre(conds) ++ getEff(effs)
......@@ -87,9 +90,7 @@ object ActionFactory {
def build(op: Op, resolver: Resolver, model: Model): ActionTemplate = {
implicit val predef: PddlPredef = resolver.predef
val pre = preProcess(op, resolver, model)
val optimizedAssertions = linter(pre.assertions)
postProcess(pre.copy(assertions = optimizedAssertions))
postProcess(pre)
}
def preProcess(op: Op, resolver: Resolver, model: Model): IntermediateAction = {
......@@ -114,7 +115,8 @@ object ActionFactory {
case Ass(All, e: TimedEqualAssertion) =>
add(Equals(ClosedInterval(start, end)), e)
case Ass(Start, e: TimedAssignmentAssertion) =>
add(Equals(LeftOpenInterval(start, BinaryExprTree(operators.Add, start, predef.Epsilon))), e)
add(Equals(LeftOpenInterval(start, BinaryExprTree(operators.Add, start, predef.Epsilon))),
e)
case Ass(End, e: TimedAssignmentAssertion) =>
add(Equals(LeftOpenInterval(end, BinaryExprTree(operators.Add, end, predef.Epsilon))), e)
case _ => unexpected
......@@ -127,20 +129,6 @@ object ActionFactory {
case class Reqs(fluent: TimedExpr, cond: Seq[Val], effs: Seq[Val]) {
override def toString: String = s"$fluent\n ${cond.mkString(" ")}\n ${effs.mkString(" ")}"
}
val linter: PASS = asss => {
val reqs = asss.groupBy(_.ass.fluent).map {
case (fluent, s) =>
val (conds, effs) = s.foldLeft((List[Val](), List[Val]())) {
case ((cs, es), Ass(t, TimedEqualAssertion(_, v, _, _))) => (Val(t, v) :: cs, es)
case ((cs, es), Ass(t, TimedAssignmentAssertion(_, v, _, _))) => (cs, Val(t, v) :: es)
case _ => unexpected
}
Reqs(fluent, conds, effs)
}
println( )
reqs.foreach(println)
asss
}
}
......@@ -153,5 +141,7 @@ object TQual {
case class Ass(qual: TQual, ass: TimedAssertion)
case class IntermediateAction(base: ActionTemplate, start: LocalVar, end: LocalVar, assertions: Seq[Ass])
case class IntermediateAction(base: ActionTemplate,
start: LocalVar,
end: LocalVar,
assertions: Seq[Ass])
package dahu.planning.pddl.parser
case class Options(discretization: Int = 1)
case class Options(discretization: Int = 1, lint: Boolean = false, optimize: Boolean = true)
......@@ -2,12 +2,13 @@ package dahu.planning.pddl.parser
import java.io.File
import com.sun.net.httpserver.Authenticator.Failure
import dahu.planning.model.core.CoreModel
import dahu.planning.model.full.Model
import dahu.planning.model.transforms.FullToCore
import dahu.planning.pddl.parser.optim.ActionRewrite
import scala.util.Try
import scala.util.{Failure, Success, Try}
class Parser(opt: Options) {
......@@ -25,11 +26,10 @@ class Parser(opt: Options) {
def parse(domain: File, problem: File): Try[CoreModel] = {
parseToFull(domain, problem).flatMap { m =>
Try {
val opt = ActionRewrite.optimize(m)
FullToCore.trans(opt)
}
if(opt.optimize)
new ActionRewrite(opt).optimize(m).map(FullToCore.trans(_))
else
Try(FullToCore.trans(m))
}
}
}
package dahu.planning.pddl.parser.optim
import dahu.planning.model.common.Interval.OpenOnRight
import dahu.planning.model.common._
import dahu.planning.model.full._
import dahu.planning.pddl.parser.PddlPredef
import dahu.planning.pddl.parser.{Options, PddlPredef}
import spire.syntax.cfor
import scala.annotation.tailrec
import scala.collection.mutable
import scala.util.Try
trait ModelOptimizer {
def optimize(model: Model): Model
}
object ActionRewrite extends ModelOptimizer {
override def optimize(model: Model): Model = {
class ActionRewrite(options: Options) {
def optimize(model: Model)(implicit predef: Predef): Try[Model] = Try {
implicit val ctx: Ctx = model
val f: InModuleBlock => InModuleBlock = {
case e: ActionTemplate => opt(e)
case x => x
......@@ -21,43 +20,84 @@ object ActionRewrite extends ModelOptimizer {
model.map(f)
}
def opt(a: ActionTemplate): ActionTemplate = {
def println(str: Any): Unit = Predef.println(str.toString.replaceAll(a.name + ".", ""))
println(a)
def opt(a: ActionTemplate)(implicit predef: Predef, ctx: Ctx): ActionTemplate = {
def println(str: Any): Unit = Predef.println(str.toString.replaceAll(a.name + "\\.", ""))
val timelines = a.store.blocks
.collect { case x: TemporallyQualifiedAssertion => x }
.map(assertionToTimeline)
.sortBy(_.toString)
val regrouped = regroup(timelines).sortBy(_.toString)
timelines.foreach(println)
println(" ============ ")
regrouped.foreach(println)
println("")
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("")
}
// println(xx)
a
}
private def tqa(itv: Interval[StaticExpr], assertion: TimedAssertion): TemporallyQualifiedAssertion =
def removeDiscontinuitiesUnsafe(timelines: Seq[Timeline],
start: StaticExpr,
end: StaticExpr): Seq[Timeline] = {
val ordering: (StaticExpr, StaticExpr) => PartialOrdering = {
case (l, r) if l == start && r == end => After
case (l, r) if r == start && l == end => Before
case _ => Unordered
}
timelines.groupBy(_.fluent).values.toSeq.map {
case Seq(tl) => tl
case Seq(tl1, tl2) =>
tl1.order(tl2, ordering) match {
case After => ???
case Before => ???
case Unordered => ???
}
}
}
private def tqa(itv: Interval[StaticExpr],
assertion: TimedAssertion): TemporallyQualifiedAssertion =
TemporallyQualifiedAssertion(Equals(itv), assertion)
def encode(tl: Timeline)(implicit predef: Predef): Seq[TemporallyQualifiedAssertion] = {
def encode(tl: Timeline)(implicit predef: Predef, ctx: Ctx): Seq[TemporallyQualifiedAssertion] = {
val fluent = tl.fluent
def go(toks: List[TToken]): List[TemporallyQualifiedAssertion] = toks match {
case TToken(itv, Is(v)) :: rest =>
tqa(itv, TimedEqualAssertion(tl.fluent, v, null, null)) :: go(rest)
def id(): Id = ctx.scope.makeNewId()
def go(toks: List[Token]): List[TemporallyQualifiedAssertion] = 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)
case Undef(itv) :: Becomes(a, v) :: rest =>
if(itv.isLeftOpen)
tqa(LeftOpenInterval(itv.start, a),
TimedAssignmentAssertion(tl.fluent, v, Some(ctx), id())) :: go(rest)
else
tqa(ClosedInterval(itv.start, a), TimedAssignmentAssertion(tl.fluent, v, Some(ctx), id())) :: go(
rest)
case Becomes(a, v) :: rest =>
tqa(Point(a), TimedAssignmentAssertion(tl.fluent, v, Some(ctx), id())) :: go(rest)
case Is(itv, v) :: rest =>
tqa(itv, TimedEqualAssertion(tl.fluent, v, Some(ctx), id())) :: go(rest)
case Nil => Nil
}
go(tl.toks.toList)
}
@tailrec def regroup(timelines: Seq[Timeline]): Seq[Timeline] = {
@tailrec private def regroup(timelines: Seq[Timeline]): Seq[Timeline] = {
val processed = mutable.Set[Timeline]()
val res = mutable.ArrayBuffer[Timeline]()
for(tl <- timelines; cand <- timelines) {
if(tl == cand || processed(tl) || processed(cand)) {
} else {
if(tl == cand || processed(tl) || processed(cand)) {} else {
tl.tryMerge(cand) match {
case Some(combined) => res += combined
case Some(combined) =>
res += combined
processed += tl
processed += cand
case None =>
......@@ -74,25 +114,28 @@ object ActionRewrite extends ModelOptimizer {
def assertionToTimeline(e: TemporallyQualifiedAssertion): Timeline = e match {
case TemporallyQualifiedAssertion(Equals(itv), TimedEqualAssertion(f, v, _, _)) =>
Timeline(f, TToken(itv, Is(v)))
Timeline(f, Is(itv, v))
case TemporallyQualifiedAssertion(Equals(itv), TimedAssignmentAssertion(f, v, _, _)) =>
itv match {
case Point(t) => Timeline(f, TToken(Point(t), Becomes(v)))
case ClosedInterval(s, e) => Timeline(f, TToken(RightOpenInterval(s,e), Undef), TToken(Point(e), Becomes(v)))
case LeftOpenInterval(s, e) => Timeline(f, TToken(OpenInterval(s,e), Undef), TToken(Point(e), Becomes(v)))
case Point(t) => Timeline(f, Becomes(t, v))
case ClosedInterval(s, e) =>
Timeline(f, Undef(RightOpenInterval(s, e)), Becomes(e, v))
case LeftOpenInterval(s, e) =>
Timeline(f, Undef(OpenInterval(s, e)), Becomes(e, v))
case _ => ???
}
case TemporallyQualifiedAssertion(Equals(itv), TimedTransitionAssertion(f, from, to, _, _)) =>
itv match {
case Point(_) => ???
case ClosedInterval(s, e) => Timeline(
f,
TToken(Point(s), Is(from)),
TToken(OpenInterval(s, e), Undef),
TToken(Point(e), Becomes(to))
)
case ClosedInterval(s, e) =>
Timeline(
f,
Is(Point(s), from),
Undef(OpenInterval(s, e)),
Becomes(e, to)
)
case _ => ???
}
......@@ -100,28 +143,30 @@ object ActionRewrite extends ModelOptimizer {
}
object Point {
def apply[A](a: A): Interval[A] = ClosedInterval(a,a)
def apply[A](a: A): Interval[A] = ClosedInterval(a, a)
def unapply[A](arg: Interval[A]): Option[A] = arg match {
case ClosedInterval(a, b) if a == b => Some(a)
case _ => None
case _ => None
}
}
sealed trait Token
case object Undef extends Token
case class Becomes(v: StaticExpr) extends Token
case class Is(v: StaticExpr) extends Token
sealed trait AfterIs
sealed trait Token {
def itv: Interval[StaticExpr]
def rightBefore(next: Token): Boolean =
itv.end == next.itv.start && itv.isRightOpen != next.itv.isLeftOpen
case class TToken(itv: Interval[StaticExpr], tok: Token) {
def rightBefore(next: TToken): Boolean = itv.end == next.itv.start && itv.isRightOpen != next.itv.isLeftOpen
override def toString: String = s"$itv $tok"
}
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 Is(itv: Interval[StaticExpr], v: StaticExpr) extends Token
class Timeline(val fluent: TimedExpr, val toks: Seq[TToken]) {
class Timeline(val fluent: TimedExpr, val toks: Seq[Token]) {
// timeline must be continuous
require(toks.nonEmpty)
require((1 until toks.size).forall(i => toks(i-1).rightBefore(toks(i))))
require((1 until toks.size).forall(i => toks(i - 1).rightBefore(toks(i))))
override def toString: String = s"$fluent: ${toks.mkString(" -- ")}"
......@@ -151,8 +196,8 @@ class Timeline(val fluent: TimedExpr, val toks: Seq[TToken]) {
}
}
object Timeline {
def apply(fluent: TimedExpr, toks: TToken*): Timeline = new Timeline(fluent, toks.toVector)
def unapply(tl: Timeline): Option[(TimedExpr, Seq[TToken])] = Some((tl.fluent, tl.toks))
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))
}
sealed trait PartialOrdering
......@@ -161,4 +206,3 @@ case object RightBefore extends PartialOrdering
case object Unordered extends PartialOrdering
case object After extends PartialOrdering
case object Before extends PartialOrdering
......@@ -9,7 +9,14 @@ import dahu.utils.Vec
import scala.concurrent.duration._
import scala.util.{Failure, Success}
case class Config(problemFile: File = null,
sealed trait Mode
object Mode {
case object Planner extends Mode
case object Linter extends Mode
}
case class Config(mode: Mode = Mode.Planner,
problemFile: File = null,
domainFile: Option[File] = None,
minInstances: Int = 0,
maxInstances: Int = 500,
......@@ -36,13 +43,15 @@ object Main extends App {
opt[Int]("discretization")
.action((i, c) => c.copy(discretization = i))
arg[File]("XXX.dom.pddl").optional().action {
case (f, c) => c.copy(domainFile = Some(f))
arg[File]("[XXX.dom.pddl] XXX.YY.pb.pddl").minOccurs(1).maxOccurs(2).action {
case (f, cfg) if cfg.problemFile == null => cfg.copy(problemFile = f)
case (f, cfg) => cfg.copy(domainFile = Some(cfg.problemFile), problemFile = f)
}
arg[File]("XXXX.YY.pb.pddl").action {
case (f, cfg) => cfg.copy(problemFile = f)
}
cmd("lint")
.text("Analyzes the domain and problem for common problems and possible optimizations.")
.action((_, cfg) => cfg.copy(mode = Mode.Linter))
}
optionsParser.parse(args, Config()) match {
......@@ -59,10 +68,22 @@ object Main extends App {
sys.exit(1)
}
}
solve(dom, pb, cfg)
cfg.mode match {
case Mode.Planner => solve(dom, pb, cfg)
case Mode.Linter => lint(dom, pb, cfg)
}
case None => sys.exit(1)
}
def lint(domain: File, problem: File, cfg: Config): Unit = {
val pddlOptions = Options(discretization = cfg.discretization, lint = true)
val parser = new Parser(pddlOptions)
implicit val predef: PddlPredef = parser.predef
parser.parse(domain, problem)
}
type Plan = String
def solve(domain: File, problem: File, config: Config): Option[Plan] = {
val pddlOptions = Options(discretization = config.discretization)
......
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