TransitionSystemParser.scala 2.88 KB
Newer Older
1 2 3 4 5
package de.tum.niwo.parser

import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FOLTL._
Christian Müller's avatar
Christian Müller committed
6
import ParserUtils._
7
import de.tum.niwo.parser.TransitionSystemParser.repsep
Christian Müller's avatar
Christian Müller committed
8
import de.tum.niwo.parser.WorkflowParser.{TYPEDVAR, repsep}
9 10 11 12

import scala.util.parsing.combinator.{PackratParsers, RegexParsers}

object TransitionSystemParser extends RegexParsers
Christian Müller's avatar
Christian Müller committed
13
  with PackratParsers with FormulaParser with LazyLogging {
14 15 16 17

  private def BLOCKLIST:Parser[List[TSBlock]] = (BLOCK | LOOP | NDCHOICE)+
  private def LOOP: Parser[TSLoop] = "loop" ~> "{" ~> BLOCKLIST <~ "}" ^^ (bs => TSLoop(bs))
  private def NDCHOICE: Parser[TSNondetChoice] =
18
    "choose" ~> "{" ~> (BLOCKLIST <~ "}" <~ "{") ~ BLOCKLIST <~ "}" ^^  {
19 20 21 22 23 24 25 26 27 28 29 30 31
      case l ~ r => TSNondetChoice(l,r)
  }

  private def SETSTMT: Parser[SetStmt] = (FUN <~ ":=") ~ TERM ^^ {
    case fun ~ guard => SetStmt(guard, fun.name, fun.params)
  }

  private def BLOCK:Parser[TSBlock] = "sim {" ~> (SETSTMT+) <~ "}" ^^ {
    stmts => SimpleTSBlock(stmts)
  } | SETSTMT ^^ {
    stmt => SimpleTSBlock(List(stmt))
  }

32 33
  private def PREDLIST: PackratParser[Set[Fun]] = rep1sep(FUN,",") ^^ { l => l.toSet } | "-" ^^^ {Set[Fun]()}
  private def VARLIST: PackratParser[Set[Var]] = rep1sep(TYPEDVAR, ",") ^^ { l => l.toSet } | "-" ^^^ {Set[Var]()}
34

35
  private lazy val SIG:PackratParser[Signature] =
36 37 38 39
    ("EmptyPredicates:" ~> PREDLIST) ~
    ("AxiomPredicates:" ~> PREDLIST) ~
    ("As:" ~> PREDLIST) ~
    ("Bs:" ~> PREDLIST) ~
40 41
    ("Constants:" ~> VARLIST) ^^ {
      case preds ~ constas ~ as ~ bs ~ consts => Signature(as, constas, bs, preds, consts)
42 43
    }

44
  private def SPEC: PackratParser[InvariantSpec] =
45 46
    ("Signature" ~> SIG) ~
    ("Transition System" ~> BLOCKLIST) ~
47
    ("Invariant" ~> repsep(TERM, ",")) ~
Christian Müller's avatar
Christian Müller committed
48
    (("Universe" ~> repsep(TYPEDVAR, ","))?) ~
49
    (("Axioms" ~> repsep(TERM, ","))?)^? {
Christian Müller's avatar
Christian Müller committed
50
      case sig ~ blocks ~ invariants ~ universe ~ axioms if {
51
        val infered = blocks.map(ParserUtils.inferBlockTypeFromSig(sig, _))
Christian Müller's avatar
Christian Müller committed
52
        val predicates = allpredicates(infered)
53 54 55 56 57 58 59 60

        val axiomlist = axioms.toList.flatten
        val inferedaxioms = axiomlist.map(a => inferFormulaTypes(sig, a))
        val inferedinvs = invariants.map(i => inferFormulaTypes(sig, i))

        checkSig(sig, predicates) &&
        inferedaxioms.forall(checkSig(sig, _))
        inferedinvs.forall(checkSig(sig, _))
Christian Müller's avatar
Christian Müller committed
61
      } => {
62 63
        // TODO: Beautify
        val infered = blocks.map(ParserUtils.inferBlockTypeFromSig(sig, _))
Christian Müller's avatar
type  
Christian Müller committed
64
        val axiomlist = axioms.toList.flatten
65 66 67
        val inferedaxioms = axiomlist.map(a => inferFormulaTypes(sig, a))
        val inferedinvs = invariants.map(i => inferFormulaTypes(sig, i))

Christian Müller's avatar
Christian Müller committed
68
        val ts = TransitionSystem(sig, infered)
69
        InvariantSpec(
Christian Müller's avatar
Christian Müller committed
70
          ts, And.make(inferedaxioms), And.make(inferedinvs), universe
71 72 73 74
        )
      }
    }

75
  def parseSpec(s: String): ParseResult[InvariantSpec] = parseAll(phrase(SPEC), s)
76
}