TransitionSystemParser.scala 2.76 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
8 9 10 11

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

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

  private def BLOCKLIST:Parser[List[TSBlock]] = (BLOCK | LOOP | NDCHOICE)+
  private def LOOP: Parser[TSLoop] = "loop" ~> "{" ~> BLOCKLIST <~ "}" ^^ (bs => TSLoop(bs))
  private def NDCHOICE: Parser[TSNondetChoice] =
17
    "choose" ~> "{" ~> (BLOCKLIST <~ "}" <~ "{") ~ BLOCKLIST <~ "}" ^^  {
18 19 20 21 22 23 24 25 26 27 28 29 30
      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))
  }

31 32
  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]()}
33

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

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

        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
59
      } => {
60 61
        // TODO: Beautify
        val infered = blocks.map(ParserUtils.inferBlockTypeFromSig(sig, _))
Christian Müller's avatar
type  
Christian Müller committed
62
        val axiomlist = axioms.toList.flatten
63 64 65
        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
66
        val ts = TransitionSystem(sig, infered)
67
        InvariantSpec(
68
          ts, And.make(inferedaxioms), And.make(inferedinvs)
69 70 71 72
        )
      }
    }

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