Main.hs 7.52 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
checkStrongConsensus :: PopulationProtocol -> OptIO PropResult
checkStrongConsensus pp = do
95
        r <- checkStrongConsensus' pp [] []
96
        case r of
97
98
            (Nothing, _, _) -> return Satisfied
            (Just _, _, _) -> return Unknown
99

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

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

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

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

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

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

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

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

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