...
 
Commits (6)
......@@ -23,7 +23,7 @@ executable peregrine
other-modules:
-- other-extensions:
build-depends: base >=4 && <5, sbv, parsec >= 3.1, containers, transformers,
bytestring, mtl, stm, async, parallel-io, text, aeson
bytestring, mtl, stm, async, parallel-io, text, aeson, process
hs-source-dirs: src
default-language: Haskell2010
ghc-options: -fsimpl-tick-factor=1000 -threaded -rtsopts -with-rtsopts=-N
{-# LANGUAGE OverloadedStrings #-}
module Main where
import System.Exit
......@@ -23,6 +25,14 @@ import StructuralComputation
import Solver
import Solver.LayeredTermination
import Solver.StrongConsensus
import Solver.Lola
import Data.Aeson
import qualified Data.Text as T
import qualified Data.Text.Lazy.IO as T
import qualified Data.Text.Lazy.Encoding as T
import qualified Data.ByteString as B
type StrongConsensusRealCounterExample = (Configuration, Configuration, Configuration, [Transition], [Transition])
writeFiles :: String -> PopulationProtocol -> [Property] -> OptIO ()
writeFiles basename pp props = do
......@@ -95,13 +105,23 @@ printInvariant inv = do
checkStrongConsensus :: Bool -> PopulationProtocol -> OptIO PropResult
checkStrongConsensus checkCorrectness pp = do
r <- checkStrongConsensus' checkCorrectness pp ([], [])
r <- checkStrongConsensus' checkCorrectness pp ([], [], [])
case r of
(Nothing, _) -> return Satisfied
(Just _, _) -> return Unknown
writeCounterExample :: PopulationProtocol -> StrongConsensusRealCounterExample -> IO ()
writeCounterExample pp (c0, c1, c2, t1, t2) = do
s <- doesSatisfy pp c1
let (c, t) = if s then (c1, t1) else (c2, t2)
let output = object [ "c0" .= map T.pack (verboseShow c0)
, "c1" .= map T.pack (verboseShow c)
, "t" .= map T.pack (map show t)]
T.writeFile "/tmp/peregrine-counterexample" $ T.decodeUtf8 $ encode $ output
checkStrongConsensus' :: Bool -> PopulationProtocol -> RefinementObjects ->
OptIO (Maybe StrongConsensusCounterExample, RefinementObjects)
OptIO (Maybe StrongConsensusRealCounterExample, RefinementObjects)
checkStrongConsensus' checkCorrectness pp refinements = do
optRefine <- opt optRefinementType
case optRefine of
......@@ -110,7 +130,7 @@ checkStrongConsensus' checkCorrectness pp refinements = do
case r of
-- TODO unify counter example
Nothing -> return (Nothing, refinements)
Just (m0,m1,m2,x1,x2,_,_,_,_) -> return (Just (m0,m1,m2,x1,x2), refinements)
Just (m0,m1,m2,x1,x2,_,_,_,_) -> return (Nothing, refinements) --return (Just (m0,m1,m2,x1,x2), refinements)
_ -> do
r <- checkSat $ checkStrongConsensusSat checkCorrectness pp refinements
case r of
......@@ -126,8 +146,26 @@ checkStrongConsensus' checkCorrectness pp refinements = do
refineStrongConsensus :: Bool -> PopulationProtocol -> [RefinementType] -> RefinementObjects ->
StrongConsensusCounterExample ->
OptIO (Maybe StrongConsensusCounterExample, RefinementObjects)
refineStrongConsensus _ _ [] refinements c = return (Just c, refinements)
OptIO (Maybe StrongConsensusRealCounterExample, RefinementObjects)
refineStrongConsensus checkCorrectness pp [] refinements c = do
let (c0, c1, c2, _, _ ) = c
reachSeq <- liftIO $ sequence [y | c' <- [c1, c2],
let y = do
ts <- getReachSequence pp c0 c'
return (c0, ts, c')
]
let nonReachConstraints = [(c0, c') | (c0, Nothing, c') <- reachSeq]
case nonReachConstraints of
[] -> do
let [(_, Just t1, _), (_, Just t2, _)] = reachSeq
let c' = (c0, c1, c2, t1, t2)
liftIO $ writeCounterExample pp c'
return (Just c', refinements)
xs -> do
let (traps, siphons, nonreach) = refinements
let refinements' = (traps, siphons, xs ++ nonreach)
checkStrongConsensus' checkCorrectness pp refinements'
refineStrongConsensus checkCorrectness pp (ref:refs) refinements c = do
let refinementMethod = case ref of
TrapRefinement -> Solver.StrongConsensus.findTrapConstraintsSat
......@@ -139,12 +177,12 @@ refineStrongConsensus checkCorrectness pp (ref:refs) refinements c = do
Nothing -> do
refineStrongConsensus checkCorrectness pp refs refinements c
Just refinement -> do
let (utraps, usiphons) = refinements
let (utraps, usiphons, nonreach) = refinements
let refinements' = case ref of
TrapRefinement -> (refinement:utraps, usiphons)
SiphonRefinement -> (utraps, refinement:usiphons)
UTrapRefinement -> (refinement:utraps, usiphons)
USiphonRefinement -> (utraps, refinement:usiphons)
TrapRefinement -> (refinement:utraps, usiphons, nonreach)
SiphonRefinement -> (utraps, refinement:usiphons, nonreach)
UTrapRefinement -> (refinement:utraps, usiphons, nonreach)
USiphonRefinement -> (utraps, refinement:usiphons, nonreach)
checkStrongConsensus' checkCorrectness pp refinements'
checkLayeredTermination :: PopulationProtocol -> OptIO PropResult
......@@ -185,7 +223,7 @@ main = do
Satisfied ->
exitSuccessWith $ "All properties " ++ show r
_ ->
exitFailureWith $ "Some properties " ++ show r
exitSuccessWith $ "Some properties " ++ show r
exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
......
......@@ -24,6 +24,7 @@ data RefinementType = TrapRefinement
| SiphonRefinement
| UTrapRefinement
| USiphonRefinement
| NonReachRefinement
deriving (Show,Read)
data PropertyOption = PropDefault
......
......@@ -27,13 +27,13 @@ languageDef =
Token.commentStart = "/*",
Token.commentEnd = "*/",
Token.commentLine = "//",
Token.identStart = letter <|> char '_',
Token.identStart = alphaNum <|> letter <|> char '_',
Token.identLetter = alphaNum <|> char '_',
Token.reservedNames = ["true", "false", "EXISTS", "FORALL"],
Token.reservedOpNames = ["->", "<", "<=", "=", "!=", ">=", ">",
"+", "-", "*", "&&", "||", "!", ":"]
}
lexer :: Token.TokenParser ()
lexer = Token.makeTokenParser languageDef
......@@ -71,7 +71,7 @@ numberOption :: Parser Integer
numberOption = option 1 (brackets natural)
ident :: Parser String
ident = (identifier <|> stringLiteral) <?> "identifier"
ident = (char 'C' *> brackets (identifier <|> stringLiteral)) <?> "identifier"
identList :: Parser [String]
identList = singleOrList ident
......@@ -152,13 +152,13 @@ instance FromJSON (QuantFormula String) where
instance ToJSON (QuantFormula String) where
toJSON x = String ""
data RecordTransition = RecordTransition {
data RecordTransition = RecordTransition {
name :: String,
pre :: [String],
post :: [String]
} deriving (Show)
data RecordPP = RecordPP {
data RecordPP = RecordPP {
title :: String,
states :: [String],
transitions :: [RecordTransition],
......@@ -172,20 +172,18 @@ $(deriveJSON defaultOptions ''RecordTransition)
$(deriveJSON defaultOptions ''RecordPP)
recordPP2PopulationProtocol :: RecordPP -> PopulationProtocol
recordPP2PopulationProtocol r =
recordPP2PopulationProtocol r =
makePopulationProtocolFromStrings (title r) (states r) (map name (transitions r)) (initialStates r) (trueStates r) falseStates p arcs where
falseStates = [q | q <- states r, not (S.member q (S.fromList (trueStates r)))]
arcs = [(q, name t, 1) | t <- transitions r, q <- pre t] ++
arcs = [(q, name t, 1) | t <- transitions r, q <- pre t] ++
[(name t, q, 1) | t <- transitions r, q <- post t]
p = case predicate r of Nothing -> ExQuantFormula [] FTrue
p = case predicate r of Nothing -> ExQuantFormula [] FTrue
(Just p') -> p'
parseContent :: Parser PopulationProtocol
parseContent = do
parseContent = do
str <- manyTill anyChar eof
let r = eitherDecode (BS.pack str)
case r of
(Left e) -> fail e
(Right pp) -> return (recordPP2PopulationProtocol pp)
{-# LANGUAGE OverloadedStrings #-}
module Solver.Lola (getReachSequence, markedPP2Lola)
where
import Data.List (intercalate)
import Util
import Solver.StrongConsensus
import PopulationProtocol
import qualified Data.Text as T
import qualified Data.Map.Strict as M
import System.Process
markedPP2Lola :: PopulationProtocol -> Configuration -> [String]
markedPP2Lola pp c = [ showPlaces,
showMarking c,
unlines [showTransition t i | (t, i) <- zip (transitions pp) [1..]]
]
where
showPlaces = "PLACE " ++ intercalate "," (show <$> states pp) ++ ";"
showMarking m = "MARKING " ++ intercalate "," [show s ++ ": " ++ show i | (s,i) <- items m] ++ ";"
showTransition t i = "TRANSITION " ++ show i ++ "\n" ++
"CONSUME " ++ intercalate "," [show s ++ ": " ++ show i | (s, i) <- lpre pp t] ++ ";\n" ++
"PRODUCE " ++ intercalate "," [show s ++ ": " ++ show i | (s, i) <- lpost pp t] ++ ";\n"
marking2Lola :: Configuration -> String
marking2Lola c = "(" ++ intercalate " AND " [show s ++ " = " ++ show i | (s, i) <- items c] ++ ")"
getReachSequence :: PopulationProtocol -> Configuration -> Configuration -> IO (Maybe [Transition])
getReachSequence pp c c' = do
str <- readCreateProcess (shell reachRequest) petriNet
let transDict = M.fromList $ zip [1..] $ transitions pp
let transitions = (M.!) transDict <$> ((read <$> lines str) :: [Int])
return $ case transitions of
[] -> Nothing
_ -> Just transitions
where
reachRequest = "lola --path=/dev/stdout --quiet -f \"REACHABLE " ++ marking2Lola c' ++ "\""
petriNet = unlines $ markedPP2Lola pp c
{-# LANGUAGE FlexibleContexts #-}
module Solver.StrongConsensus
(checkStrongConsensusSat,
(doesSatisfy, --TODO: REMOVE
checkStrongConsensusSat,
checkStrongConsensusCompleteSat,
StrongConsensusCounterExample,
RefinementObjects,
......@@ -13,7 +14,7 @@ where
import Data.SBV
import qualified Data.Map as M
import Data.List ((\\),genericLength)
import Data.List ((\\), genericLength)
import Util
import PopulationProtocol
......@@ -23,7 +24,7 @@ import Solver.Formula
type StrongConsensusCounterExample = (Configuration, Configuration, Configuration, FlowVector, FlowVector)
type StrongConsensusCompleteCounterExample = (Configuration, Configuration, Configuration, FlowVector, FlowVector, Configuration, Configuration, Configuration, Configuration)
type RefinementObjects = ([Trap], [Siphon])
type RefinementObjects = ([Trap], [Siphon], [(Configuration, Configuration)])
stateEquationConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap Transition -> SBool
stateEquationConstraints pp m0 m x =
......@@ -50,6 +51,24 @@ initialConfiguration pp m0 =
(sum (mval m0 (initialStates pp)) .>= 2) &&&
(sum (mval m0 (states pp \\ initialStates pp)) .== 0)
doesSatisfy :: PopulationProtocol -> Configuration -> IO Bool
doesSatisfy pp c = do
let request = (do
m' <- sequence $ sInteger <$> map show (states pp)
let m = M.fromList (zip (states pp) m') :: SIMap State
let eqC = bAnd [val m q .== (fromInteger (val c q)) | q <- states pp]
let ev = if null (quantifiedVariables (predicate pp)) then
evaluateFormula (innerFormula (predicate pp)) m
else
evaluateFormula (innerFormula (predicate pp)) m
return ev)
res <- sat request
case res of
SatResult (Satisfiable _ _ ) -> return True
_ -> return False
differentConsensusConstraints :: Bool -> PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap State -> SIMap State -> SBool
differentConsensusConstraints checkCorrectness pp m0 m1 m2 qe qa =
(oT &&& oF) |||
......@@ -103,8 +122,8 @@ checkUSiphonConstraints pp m0 m1 m2 x1 x2 siphons =
bAnd $ map (checkUSiphon pp m0 m1 m2 x1 x2) siphons
checkStrongConsensus :: Bool -> PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition ->
SIMap State -> SIMap State ->RefinementObjects -> SBool
checkStrongConsensus checkCorrectness pp m0 m1 m2 x1 x2 qe qa (utraps, usiphons) =
SIMap State -> SIMap State -> RefinementObjects -> SBool
checkStrongConsensus checkCorrectness pp m0 m1 m2 x1 x2 qe qa (utraps, usiphons, nonreach) =
stateEquationConstraints pp m0 m1 x1 &&&
stateEquationConstraints pp m0 m2 x2 &&&
initialConfiguration pp m0 &&&
......@@ -117,7 +136,13 @@ checkStrongConsensus checkCorrectness pp m0 m1 m2 x1 x2 qe qa (utraps, usiphons)
terminalConstraints pp m2 &&&
differentConsensusConstraints checkCorrectness pp m0 m1 m2 qe qa &&&
checkUTrapConstraints pp m0 m1 m2 x1 x2 utraps &&&
checkUSiphonConstraints pp m0 m1 m2 x1 x2 usiphons
checkUSiphonConstraints pp m0 m1 m2 x1 x2 usiphons &&&
nonReachConstraints pp m0 m1 m2 nonreach
nonReachConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> [(Configuration, Configuration)] -> SBool
nonReachConstraints pp m0 m1 m2 nonreach = bAnd [nonEq m0 c ||| (nonEq m1 c' &&& nonEq m2 c') | (c, c') <- nonreach] where
nonEq :: SIMap State -> Configuration -> SBool
nonEq m c = bOr [val m q ./= (fromInteger (val c q)) | q <- states pp]
checkStrongConsensusSat :: Bool -> PopulationProtocol -> RefinementObjects -> ConstraintProblem Integer StrongConsensusCounterExample
checkStrongConsensusSat checkCorrectness pp refinements =
......@@ -357,3 +382,7 @@ completeCounterExampleFromAssignment :: Integer -> IMap State -> IMap State -> I
completeCounterExampleFromAssignment max m0 m1 m2 x1 x2 r1 r2 s1 s2 =
(makeVector m0, makeVector m1, makeVector m2, makeVector x1, makeVector x2, makeVector r1, makeVector r2, makeVector s1, makeVector s2)
where maximalSet q = M.keys $ M.filter (== max) q
checkCounterExample :: StrongConsensusCounterExample -> PopulationProtocol -> Bool
checkCounterExample example pp = undefined
......@@ -5,7 +5,7 @@ module Util
listSet,listMap,val,vals,mval,zeroVal,positiveVal,sumVal,
makeVarMap,makeVarMapWith,buildVector,makeVector,getNames,
Vector,IVector,RVector,Model,VarMap,SIMap,SRMap,SBMap,IMap,RMap,BMap,showWeighted,
OptIO,verbosePut,opt,putLine,parallelIO)
OptIO,verbosePut,opt,putLine,parallelIO, verboseShow)
where
import Data.SBV
......@@ -145,3 +145,5 @@ numPref s = map (\i -> s ++ show i) [(1::Integer)..]
showWeighted :: (Show a, Num b, Eq b, Show b) => (a, b) -> String
showWeighted (x, w) = (if w == 1 then "" else show w) ++ show x
verboseShow :: Show a => Vector a Integer -> [String]
verboseShow (Vector v) = map show $ concatMap (\(x, y) -> replicate (fromIntegral y) x) (M.toList v)