Commit 38640f20 authored by Arthur Bit-Monnot's avatar Arthur Bit-Monnot

Added static predicates for RCLL.

parent 36ebd63b
......@@ -23,7 +23,7 @@ object Action {
}
val chronicle = act.content.foldLeft(Chronicle.empty(ctx)) {
case (c, s) => c.extended(s)(argsRewrite)
case (c, s) => c.extended(s, isAction = true)(argsRewrite)
}
Action(
......
......@@ -356,7 +356,22 @@ case class Chronicle(ctx: ProblemContext,
import ctx._
def extended(e: InActionBlock)(implicit argRewrite: Arg => Tentative[Literal]): Chronicle =
def isStatic(f: FunctionTemplate): Boolean = f.id.name match {
case "order-gate" => true
case "mps-type" => true
case "order-base-color" => true
case "rs-inc" => true
case "cs-free" => true
case "order-cap-color" => true
case "order-ring1-color" => true
case "path-length" => true
case "rs-sub" => true
case "order-complexity" | "rs-ring-spec" => true
case _ => false
}
def extended(e: InActionBlock, isAction: Boolean)(
implicit argRewrite: Arg => Tentative[Literal]): Chronicle =
e match {
case _: LocalVarDeclaration => this
case _: ArgDeclaration => this
......@@ -371,8 +386,17 @@ case class Chronicle(ctx: ProblemContext,
)
case TimedAssignmentAssertion(itv, fluent, value) =>
val changeItv = itv.map(encodeAsInt)
val persistenceEnd = anonymousTp().subjectTo(changeItv.end <= _)
assert(!isStatic(fluent.template) || !isAction, s"${fluent.template} is not static")
val changeItv =
if(isStatic(fluent.template))
LeftOpenInterval(ctx.temporalOrigin, ctx.temporalOrigin)
else
itv.map(encodeAsInt)
val persistenceEnd =
if(isStatic(fluent.template))
ctx.temporalHorizon
else
anonymousTp().subjectTo(changeItv.end <= _)
val token = EffectToken(
changeItv,
persistenceEnd = persistenceEnd,
......@@ -382,14 +406,20 @@ case class Chronicle(ctx: ProblemContext,
copy(effects = token :: effects)
case TimedEqualAssertion(itv, f, v) =>
val persistenceItv =
if(isStatic(f.template))
ClosedInterval(ctx.temporalOrigin, ctx.temporalHorizon)
else
itv.map(encodeAsInt)
val token = ConditionToken(
itv = itv.map(encodeAsInt),
itv = persistenceItv,
fluent = encode(f),
value = encode(v)
)
copy(conditions = token :: conditions)
case TimedTransitionAssertion(ClosedInterval(s, e), f, v1, v2) =>
assert(!isStatic(f.template), s"${f.template} is not static")
val start = encodeAsInt(s)
val changeEnd = encodeAsInt(e)
val persistenceEnd = anonymousTp().subjectTo(changeEnd <= _)
......
......@@ -61,7 +61,8 @@ object Planner {
info(" Processing ANML model...")
val ctx = ProblemContext.extract(model)
val result = model.foldLeft(Chronicle.empty(ctx)) {
case (chronicle, statement: Statement) => chronicle.extended(statement)(_ => unexpected)
case (chronicle, statement: Statement) =>
chronicle.extended(statement, isAction = false)(_ => unexpected)
case (chronicle, action: ActionTemplate) =>
val actionInstances: Seq[Opt[Action[Tentative]]] =
if(cfg.symBreak) {
......
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