Added support for mist (spec) input files

benchmarks/cav-benchmarks/run-benchmarks.sh

+#!/bin/bash
+
+#benchmarks=( 'mist' 'wahl-kroening' 'soter' )
+benchmarks=( 'soter' )
+extensions=( 'spec' )
+executable='../../slapnet'
+
+for benchmark in ${benchmarks[@]}; do
+  benchmark_dir="$benchmark"
+  >$benchmark_dir/positive-slapnet.list
+  >$benchmark_dir/dontknow-slapnet.list
+  >$benchmark_dir/timeout-slapnet.list
+  >$benchmark_dir/error-slapnet.list
+  for ext in ${extensions[@]}; do
+    for file in `find $benchmark_dir -name "*.$ext"`; do
+      T="$(date +%s%N)"
+      (
+        set -o pipefail;
+        timeout 60 $executable --$ext $file | tee $file.out
+      )
+      result=$?
+      T=$(($(date +%s%N)-T))
+      if [[ result -eq 0 ]]; then
+          list='positive'
+      elif [[ result -eq 2 ]]; then
+          list='dontknow'
+      elif [[ result -eq 124 || result -eq 137 ]]; then
+          list='timeout'
+      else
+          list='error'
+      fi
+      echo $T $file >>$benchmark_dir/$list-slapnet.list
+    done
+  done
+done

src/Main.hs

@@ -15,6 +15,7 @@ import Parser
 import qualified Parser.PNET as PNET
 import qualified Parser.LOLA as LOLA
 import qualified Parser.TPN as TPN
+import qualified Parser.MIST as MIST
 import PetriNet
 import Printer
 import qualified Printer.LOLA as LOLAPrinter
@@ -26,7 +27,7 @@ import Solver.TrapConstraints
 import Solver.TransitionInvariant
 import Solver.SComponent
 
-data InputFormat = PNET | LOLA | TPN deriving (Show,Read)
+data InputFormat = PNET | LOLA | TPN | MIST deriving (Show,Read)
 
 data NetTransformation = TerminationByReachability
                        | ValidateIdentifiers
@@ -72,6 +73,10 @@ options =
         (NoArg (\opt -> Right opt { inputFormat = TPN }))
         "Use the tpn input format"
 
+        , Option "" ["spec"]
+        (NoArg (\opt -> Right opt { inputFormat = MIST }))
+        "Use the mist input format"
+
         , Option "" ["validate-identifiers"]
         (NoArg (\opt -> Right opt {
             optTransformations = ValidateIdentifiers : optTransformations opt
@@ -174,9 +179,9 @@ writeFiles verbosity basename net props = do
                                          " to " ++ file
                 writeFile file $ LOLAPrinter.printProperty p
               ) (zip props [(1::Integer)..])
-        -- verbosePut verbosity 1 $ "Writing properties to " ++ basename ++ ".sara"
-        -- writeFile (basename ++ ".sara") $ unlines $
-        --        map (SARAPrinter.printProperty basename net) props
+        verbosePut verbosity 1 $ "Writing properties to " ++ basename ++ ".sara"
+        writeFile (basename ++ ".sara") $ unlines $
+                map (SARAPrinter.printProperty basename net) props
 
 checkFile :: Parser (PetriNet,[Property]) -> Int -> Bool ->
             [ImplicitProperty] -> [NetTransformation] ->
@@ -350,6 +355,7 @@ main = do
                                  PNET -> PNET.parseContent
                                  LOLA -> LOLA.parseContent
                                  TPN -> TPN.parseContent
+                                 MIST -> MIST.parseContent
                 let properties = reverse $ optProperties opts
                 let transformations = reverse $ optTransformations opts
                 rs <- mapM (checkFile parser verbosity refinement properties

src/Parser/MIST.hs

+module Parser.MIST
+    (parseContent)
+where
+
+import Control.Applicative ((<$>),(*>),(<*),(<*>))
+import Control.Monad (when)
+import Data.List (sortBy, groupBy)
+import Data.Function (on)
+import Data.Ord (comparing)
+import Text.Parsec
+import Text.Parsec.Language (LanguageDef, emptyDef)
+import qualified Text.Parsec.Token as Token
+
+import Parser
+import PetriNet (PetriNet,makePetriNetWithTrans)
+import Property
+
+languageDef :: LanguageDef ()
+languageDef =
+        emptyDef {
+                 Token.commentStart    = "",
+                 Token.commentEnd      = "",
+                 Token.commentLine     = "#",
+                 Token.identStart      = letter <|> char '_',
+                 Token.identLetter     = alphaNum <|> oneOf "'_",
+                 Token.reservedNames   = ["vars", "rules", "init",
+                                          "target", "invariants"],
+                 Token.reservedOpNames = ["->", "+", "-", "=", ">="]
+                 }
+
+lexer :: Token.TokenParser ()
+lexer = Token.makeTokenParser languageDef
+
+identifier :: Parser String
+identifier = Token.identifier lexer -- parses an identifier
+reserved :: String -> Parser ()
+reserved   = Token.reserved   lexer -- parses a reserved name
+reservedOp :: String -> Parser ()
+reservedOp = Token.reservedOp lexer -- parses an operator
+integer :: Parser Integer
+integer    = Token.integer    lexer -- parses an integer
+semi :: Parser String
+semi       = Token.semi       lexer -- parses a semicolon
+commaSep :: Parser a -> Parser [a]
+commaSep   = Token.commaSep   lexer -- parses a comma separated list
+commaSep1 :: Parser a -> Parser [a]
+commaSep1  = Token.commaSep1  lexer -- parses a comma separated list
+whiteSpace :: Parser ()
+whiteSpace = Token.whiteSpace lexer -- parses whitespace
+
+
+net :: Parser PetriNet
+net = do
+        reserved "vars"
+        ps <- many1 identifier
+        reserved "rules"
+        ts <- transitions
+        reserved "init"
+        (is,initTrans) <- initial
+        return $ makePetriNetWithTrans "" ps (initTrans ++ ts) is
+
+prop :: Parser Property
+prop = do
+        reserved "target"
+        ineqs <- many1 (commaSep1 ineq)
+        _ <- optionMaybe (reserved "invariants" *> invariants)
+        return $ Property "" Safety $
+                    foldl1 (:|:) $ map (foldl1 (:&:)) ineqs
+
+ineq :: Parser Formula
+ineq = do
+        x <- identifier
+        reservedOp ">="
+        c <- integer
+        return $ Atom $ LinIneq (Var x) Ge (Const c)
+
+transitions :: Parser [(String, [(String, Integer)], [(String, Integer)])]
+transitions = do
+        ts <- many1 transition
+        return $ map (\(i,(l,r)) -> ("'t" ++ show i,l,r))
+                        ([(1::Integer)..] `zip` ts)
+
+transition :: Parser ([(String, Integer)], [(String, Integer)])
+transition = do
+        lhs <- commaSep ((,) <$> identifier <* reservedOp ">=" <*> integer)
+        reservedOp "->"
+        rhs <- commaSep transitionAssignment
+        let rhs' = filter ((/=0) . snd) $
+                   map (\xs -> (fst (head xs), sum (map snd xs))) $
+                   groupBy ((==) `on` fst) $
+                   sortBy (comparing fst) $
+                   lhs ++ rhs
+        _ <- semi
+        return (lhs, rhs')
+
+transitionAssignment :: Parser (String, Integer)
+transitionAssignment = do
+        i1 <- identifier
+        reservedOp "="
+        i2 <- identifier
+        when (i1 /= i2 ++ "'")
+            (error ("identifiers not equal: " ++ i1 ++ " /= " ++ i2))
+        fac <- (reservedOp "-" *> return (-1)) <|> (reservedOp "+" *> return 1)
+        n <- integer
+        return (i2,fac*n)
+
+initial :: Parser ([(String, Integer)],
+                  [(String, [(String, Integer)], [(String, Integer)])])
+initial = do
+        xs <- commaSep1 initState
+        let inits = [(x,i) | (x,i,_) <- xs]
+        let covered = [x | (x,_,True) <- xs]
+        let initTrans = map (\(i,x) -> ("'init" ++ show i, [], [(x,1)]))
+                            ([(1::Integer)..] `zip` covered)
+        return (filter ((/=0) . snd) inits, initTrans)
+
+initState :: Parser (String, Integer, Bool)
+initState = do
+        s <- identifier
+        cover <- reservedOp "=" *> return False <|>
+                reservedOp ">=" *> return True
+        i <- integer
+        return (s,i,cover)
+
+invariants :: Parser [[(String, Integer)]]
+invariants = many1 (commaSep1 ((,) <$> identifier <* reservedOp "=" <*> integer))
+
+parseContent :: Parser (PetriNet,[Property])
+parseContent = do
+        whiteSpace
+        n <- net
+        p <- prop
+        eof
+        return (n, [p])