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

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

object TransitionSystemParser extends RegexParsers
Christian Müller's avatar
Christian Müller committed
11
  with PackratParsers with FormulaParser with LazyLogging {
12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44

  private def BLOCKLIST:Parser[List[TSBlock]] = (BLOCK | LOOP | NDCHOICE)+
  private def LOOP: Parser[TSLoop] = "loop" ~> "{" ~> BLOCKLIST <~ "}" ^^ (bs => TSLoop(bs))
  private def NDCHOICE: Parser[TSNondetChoice] =
    "choose" ~> "{" ~> (BLOCKLIST <~ "}" <~ "{") ~ (BLOCKLIST) <~ "}" ^^  {
      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))
  }

  private def PREDLIST: Parser[Set[Fun]] = repsep(FUN,",") ^^ { l => l.toSet }

  private def SIG:Parser[Signature] =
    ("EmptyPredicates" ~> PREDLIST) ~
    ("AxiomPredicates" ~> PREDLIST) ~
    ("As" ~> PREDLIST) ~
    ("Bs" ~> PREDLIST) ~
    ("Constants" ~> repsep(TYPEDVAR, ",")) ^^ {
      case preds ~ constas ~ as ~ bs ~ consts => Signature(as, constas, bs, preds, consts.toSet)
    }

  private def SPEC: Parser[InvariantSpec] =
    ("Signature" ~> SIG) ~
    ("Transition System" ~> BLOCKLIST) ~
    (("Axioms" ~> repsep(TERM, ","))?) ~
Christian Müller's avatar
Christian Müller committed
45 46 47 48 49 50
    ("Invariant" ~> repsep(TERM, ",")) ^? {
      case sig ~ blocks ~ axioms ~ invariants if {
        val infered = blocks.map(ParserUtils.inferTypeFromSig(sig, _))
        val predicates = allpredicates(infered)
        checkSig(sig, predicates)
      } => {
Christian Müller's avatar
type  
Christian Müller committed
51
        val axiomlist = axioms.toList.flatten
Christian Müller's avatar
Christian Müller committed
52 53
        val infered = blocks.map(ParserUtils.inferTypeFromSig(sig, _))
        val ts = TransitionSystem(sig, infered)
54
        InvariantSpec(
Christian Müller's avatar
Christian Müller committed
55
          ts, And.make(axiomlist), And.make(invariants)
56 57 58 59 60 61
        )
      }
    }

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