Main.hs 7.82 KB
Newer Older
1 2
module Main where

3
import System.Exit
4 5
import System.IO
import Control.Monad
6
import Control.Concurrent.ParallelIO
7
import Control.Arrow (first)
8
import Data.List (partition,minimumBy,genericLength)
9
import Data.Ord (comparing)
10
import Data.Maybe
11
import qualified Data.ByteString.Lazy as L
Philipp Meyer's avatar
Philipp Meyer committed
12
import Control.Monad.Reader
Philipp Meyer's avatar
Philipp Meyer committed
13

Philipp Meyer's avatar
Philipp Meyer committed
14
import Util
Philipp Meyer's avatar
Philipp Meyer committed
15
import Options
16
import Parser
17 18
import qualified Parser.PP as PPParser
import PopulationProtocol
19
import Printer
20
import qualified Printer.DOT as DOTPrinter
21
import Property
22
import StructuralComputation
23
import Solver
Philipp Meyer's avatar
Philipp Meyer committed
24 25
import Solver.LayeredTermination
import Solver.StrongConsensus
26

27 28
writeFiles :: String -> PopulationProtocol -> [Property] -> OptIO ()
writeFiles basename pp props = do
Philipp Meyer's avatar
Philipp Meyer committed
29
        format <- opt outputFormat
30
        verbosePut 1 $ "Writing " ++ showNetName pp ++ " to " ++
31 32 33
                                  basename ++ " in format " ++ show format
        case format of
            OutDOT ->
34
                liftIO $ L.writeFile basename $ DOTPrinter.printPopulationProtocol pp
35

36 37 38 39 40
structuralAnalysis :: PopulationProtocol -> OptIO ()
structuralAnalysis pp =  do
        verbosePut 0 $ "States             : " ++ show (length (states pp))
        verbosePut 0 $ "Transitions        : " ++ show (length (transitions pp))
        verbosePut 0 $ "Initial states     : " ++ show (length (initialStates pp))
41 42
        verbosePut 0 $ "Yes states         : " ++ show (length (trueStates pp))
        verbosePut 0 $ "No states          : " ++ show (length (falseStates pp))
Philipp Meyer's avatar
Philipp Meyer committed
43 44 45 46 47 48

checkFile :: String -> OptIO PropResult
checkFile file = do
        verbosePut 0 $ "Reading \"" ++ file ++ "\""
        format <- opt inputFormat
        let parser = case format of
49
                             InPP -> PPParser.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
50 51
        pp <- liftIO $ parseFile parser file
        props <- opt optProperties
52
        verbosePut 1 $ "Analyzing " ++ showNetName pp
Philipp Meyer's avatar
Philipp Meyer committed
53
        verbosePut 2 $
54
                "Number of states: " ++ show (length (states pp))
55
        verbosePut 2 $
56 57 58
                "Number of transitions: " ++ show (length (transitions pp))
        let pRowSize p = let (preP, postP) = context pp p in length preP + length postP
        let arcs = sum $ map pRowSize $ states pp
59 60
        verbosePut 2 $
                "Number of arcs: " ++ show arcs
Philipp Meyer's avatar
Philipp Meyer committed
61
        printStruct <- opt optPrintStructure
62 63
        when printStruct $ structuralAnalysis pp
        verbosePut 3 $ show pp
Philipp Meyer's avatar
Philipp Meyer committed
64
        output <- opt optOutput
65
        case output of
66
            Just outputfile ->
Philipp Meyer's avatar
Philipp Meyer committed
67
                writeFiles outputfile pp props
68
            Nothing -> return ()
69
        -- TODO: short-circuit? parallel?
Philipp Meyer's avatar
Philipp Meyer committed
70
        rs <- mapM (checkProperty pp) props
Philipp Meyer's avatar
Philipp Meyer committed
71
        verbosePut 0 ""
72
        return $ resultsAnd rs
73

74

75
checkProperty :: PopulationProtocol -> Property -> OptIO PropResult
Philipp Meyer's avatar
Philipp Meyer committed
76 77 78 79 80 81 82
checkProperty pp prop = do
        verbosePut 1 $ "\nChecking " ++ show prop
        r <- case prop of
                Correctness -> error "not yet implemented"
                LayeredTermination -> checkLayeredTermination pp
                StrongConsensus -> checkStrongConsensus pp
        verbosePut 0 $ show prop ++ " " ++ show r
83 84
        return r

85 86 87 88 89 90 91
printInvariant :: (Show a, Invariant a) => [a] -> OptIO ()
printInvariant inv = do
        verbosePut 0 "Invariant found"
        let invSize = map invariantSize inv
        verbosePut 2 $ "Number of atoms in invariants: " ++ show invSize ++
                " (total of " ++ show (sum invSize) ++ ")"
        mapM_ (putLine . show) inv
Philipp Meyer's avatar
Philipp Meyer committed
92

Philipp Meyer's avatar
Philipp Meyer committed
93 94 95
checkStrongConsensus :: PopulationProtocol -> OptIO PropResult
checkStrongConsensus pp = do
        r <- checkStrongConsensus' pp [] [] []
96
        case r of
97 98
            (Nothing, _, _, _) -> return Satisfied
            (Just _, _, _, _) -> return Unknown
99

Philipp Meyer's avatar
Philipp Meyer committed
100
checkStrongConsensus' :: PopulationProtocol ->
101
        [Trap] -> [Siphon] -> [StableInequality] ->
Philipp Meyer's avatar
Philipp Meyer committed
102 103 104
        OptIO (Maybe StrongConsensusCounterExample, [Trap], [Siphon], [StableInequality])
checkStrongConsensus' pp utraps usiphons inequalities = do
        r <- checkSat $ checkStrongConsensusSat pp utraps usiphons inequalities
105
        case r of
106
            Nothing -> return (Nothing, utraps, usiphons, inequalities)
107
            Just c -> do
108 109
                refine <- opt optRefinementType
                if isJust refine then
Philipp Meyer's avatar
Philipp Meyer committed
110
                    refineStrongConsensus pp utraps usiphons inequalities c
111
                else
112
                    return (Just c, utraps, usiphons, inequalities)
113

Philipp Meyer's avatar
Philipp Meyer committed
114 115 116 117 118
refineStrongConsensus :: PopulationProtocol ->
        [Trap] -> [Siphon] -> [StableInequality] -> StrongConsensusCounterExample ->
        OptIO (Maybe StrongConsensusCounterExample, [Trap], [Siphon], [StableInequality])
refineStrongConsensus pp utraps usiphons inequalities c@(m0, m1, m2, x1, x2) = do
        r1 <- checkSatMin $ Solver.StrongConsensus.findTrapConstraintsSat pp m0 m1 m2 x1 x2
119 120
        case r1 of
            Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
121
                r2 <- checkSatMin $ Solver.StrongConsensus.findUSiphonConstraintsSat pp m0 m1 m2 x1 x2
122 123
                case r2 of
                    Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
124
                        r3 <- checkSatMin $ Solver.StrongConsensus.findUTrapConstraintsSat pp m0 m1 m2 x1 x2
Philipp J. Meyer's avatar
Philipp J. Meyer committed
125
                        case r3 of
126
                            Nothing -> return (Just c, utraps, usiphons, inequalities)
Philipp J. Meyer's avatar
Philipp J. Meyer committed
127
                            Just utrap ->
Philipp Meyer's avatar
Philipp Meyer committed
128
                                checkStrongConsensus' pp (utrap:utraps) usiphons inequalities
Philipp J. Meyer's avatar
Philipp J. Meyer committed
129
                    Just usiphon ->
Philipp Meyer's avatar
Philipp Meyer committed
130
                        checkStrongConsensus' pp utraps (usiphon:usiphons) inequalities
131
            Just trap ->
Philipp Meyer's avatar
Philipp Meyer committed
132
                checkStrongConsensus' pp (trap:utraps) usiphons inequalities
133

Philipp Meyer's avatar
Philipp Meyer committed
134 135
checkLayeredTermination :: PopulationProtocol -> OptIO PropResult
checkLayeredTermination pp = do
136
        let nonTrivialTriplets = filter (not . trivialTriplet) $ generateTriplets pp
Philipp Meyer's avatar
Philipp Meyer committed
137
        checkLayeredTermination' pp nonTrivialTriplets 1 $ genericLength $ transitions pp
138

Philipp Meyer's avatar
Philipp Meyer committed
139 140
checkLayeredTermination' :: PopulationProtocol -> [Triplet] -> Integer -> Integer -> OptIO PropResult
checkLayeredTermination' pp triplets k kmax = do
141
        verbosePut 1 $ "Checking layered termination with at most " ++ show k ++ " layers"
Philipp Meyer's avatar
Philipp Meyer committed
142
        r <- checkSatMin $ checkLayeredTerminationSat pp triplets k
143
        case r of
144 145
            Nothing ->
                if k < kmax then
Philipp Meyer's avatar
Philipp Meyer committed
146
                    checkLayeredTermination' pp triplets (k + 1) kmax
147 148
                else
                    return Unknown
149 150
            Just inv -> do
                invariant <- opt optInvariant
151 152
                when invariant $ printInvariant inv
                return Satisfied
153

154
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
155
main = do
Philipp Meyer's avatar
Philipp Meyer committed
156
        putStrLn "Peregrine - Efficient Verification of Population Protocols\n"
157 158 159 160 161
        args <- parseArgs
        case args of
            Left err -> exitErrorWith err
            Right (opts, files) -> do
                when (optShowVersion opts) (exitSuccessWith "Version 0.01")
Philipp Meyer's avatar
Philipp Meyer committed
162
                when (optShowHelp opts) (exitSuccessWith usageInformation)
163
                when (null files) (exitErrorWith "No input file given")
164
                let opts' = opts { optProperties = reverse (optProperties opts) }
Philipp Meyer's avatar
Philipp Meyer committed
165
                rs <- runReaderT (mapM checkFile files) opts'
166 167
                -- TODO: short-circuit with Control.Monad.Loops? parallel
                -- execution?
Philipp Meyer's avatar
Philipp Meyer committed
168 169
                let r = resultsAnd rs
                case r of
170
                    Satisfied ->
Philipp Meyer's avatar
Philipp Meyer committed
171 172 173
                        exitSuccessWith $ "All properties " ++ show r
                    _ ->
                        exitFailureWith $ "Some properties " ++ show r
174 175 176 177

exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
178
        cleanupAndExitWith ExitSuccess
179 180 181 182

exitFailureWith :: String -> IO ()
exitFailureWith msg = do
        putStrLn msg
183
        cleanupAndExitWith $ ExitFailure 2
Philipp Meyer's avatar
Philipp Meyer committed
184

185 186 187
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
188 189 190 191 192 193
        cleanupAndExitWith $ ExitFailure 3

cleanupAndExitWith :: ExitCode -> IO ()
cleanupAndExitWith code = do
        stopGlobalPool
        exitWith code