Main.hs 9.55 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
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
--checkStrongConsensus' :: PopulationProtocol -> RefinementObjects ->
--        OptIO (Maybe StrongConsensusCounterExample, RefinementObjects)
--checkStrongConsensus' pp refinements = do
--        optRefine <- opt optRefinementType
--        let method = case optRefine of
--                        RefAll -> checkStrongConsensusCompleteSat pp
--                        _ -> checkStrongConsensusSat pp refinements
--        r <- checkSat $ method
--        case r of
--            Nothing -> return (Nothing, refinements)
--            Just c -> do
--                case optRefine of
--                        RefDefault ->
--                            let refinementMethods = [TrapRefinement, SiphonRefinement, UTrapRefinement, USiphonRefinement]
--                            in refineStrongConsensus pp refinementMethods refinements c
--                        RefList refinementMethods ->
--                            refineStrongConsensus pp refinementMethods refinements c
--                        RefAll -> return (Nothing, refinements)

119
120
121
checkStrongConsensus' :: PopulationProtocol -> RefinementObjects ->
        OptIO (Maybe StrongConsensusCounterExample, RefinementObjects)
checkStrongConsensus' pp refinements = do
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
        optRefine <- opt optRefinementType
        case optRefine of
            RefAll -> do
                r <- checkSat $ checkStrongConsensusCompleteSat pp
                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)
            _ -> do
                r <- checkSat $ checkStrongConsensusSat pp refinements
                case r of
                    Nothing -> return (Nothing, refinements)
                    Just c -> do
                        case optRefine of
                                RefDefault ->
                                    let refinementMethods = [TrapRefinement, SiphonRefinement, UTrapRefinement, USiphonRefinement]
                                    in refineStrongConsensus pp refinementMethods refinements c
                                RefList refinementMethods ->
                                    refineStrongConsensus pp refinementMethods refinements c
                                RefAll -> return (Nothing, refinements)
142
143
144
145
146
147
148
149
150
151
152
153
154

refineStrongConsensus :: PopulationProtocol -> [RefinementType] -> RefinementObjects ->
        StrongConsensusCounterExample ->
        OptIO (Maybe StrongConsensusCounterExample, RefinementObjects)
refineStrongConsensus pp [] refinements c = return (Just c, refinements)
refineStrongConsensus pp (ref:refs) refinements c = do
        let refinementMethod = case ref of
                         TrapRefinement -> Solver.StrongConsensus.findTrapConstraintsSat
                         SiphonRefinement -> Solver.StrongConsensus.findSiphonConstraintsSat
                         UTrapRefinement -> Solver.StrongConsensus.findUTrapConstraintsSat
                         USiphonRefinement -> Solver.StrongConsensus.findUSiphonConstraintsSat
        r <- checkSatMin $ refinementMethod pp c
        case r of
155
            Nothing -> do
156
157
158
159
160
161
162
163
164
                refineStrongConsensus pp refs refinements c
            Just refinement -> do
                let (utraps, usiphons) = refinements
                let refinements' = case ref of
                         TrapRefinement -> (refinement:utraps, usiphons)
                         SiphonRefinement -> (utraps, refinement:usiphons)
                         UTrapRefinement -> (refinement:utraps, usiphons)
                         USiphonRefinement -> (utraps, refinement:usiphons)
                checkStrongConsensus' pp refinements'
165

Philipp Meyer's avatar
Philipp Meyer committed
166
167
checkLayeredTermination :: PopulationProtocol -> OptIO PropResult
checkLayeredTermination pp = do
168
        let nonTrivialTriplets = filter (not . trivialTriplet) $ generateTriplets pp
Philipp Meyer's avatar
Philipp Meyer committed
169
        checkLayeredTermination' pp nonTrivialTriplets 1 $ genericLength $ transitions pp
170

Philipp Meyer's avatar
Philipp Meyer committed
171
172
checkLayeredTermination' :: PopulationProtocol -> [Triplet] -> Integer -> Integer -> OptIO PropResult
checkLayeredTermination' pp triplets k kmax = do
173
        verbosePut 1 $ "Checking layered termination with at most " ++ show k ++ " layers"
Philipp Meyer's avatar
Philipp Meyer committed
174
        r <- checkSatMin $ checkLayeredTerminationSat pp triplets k
175
        case r of
176
177
            Nothing ->
                if k < kmax then
Philipp Meyer's avatar
Philipp Meyer committed
178
                    checkLayeredTermination' pp triplets (k + 1) kmax
179
180
                else
                    return Unknown
181
182
            Just inv -> do
                invariant <- opt optInvariant
183
184
                when invariant $ printInvariant inv
                return Satisfied
185

186
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
187
main = do
Philipp Meyer's avatar
Philipp Meyer committed
188
        putStrLn "Peregrine - Efficient Verification of Population Protocols\n"
189
190
191
192
193
        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
194
                when (optShowHelp opts) (exitSuccessWith usageInformation)
195
                when (null files) (exitErrorWith "No input file given")
196
                rs <- runReaderT (mapM checkFile files) opts
197
198
                -- TODO: short-circuit with Control.Monad.Loops? parallel
                -- execution?
Philipp Meyer's avatar
Philipp Meyer committed
199
200
                let r = resultsAnd rs
                case r of
201
                    Satisfied ->
Philipp Meyer's avatar
Philipp Meyer committed
202
203
204
                        exitSuccessWith $ "All properties " ++ show r
                    _ ->
                        exitFailureWith $ "Some properties " ++ show r
205
206
207
208

exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
209
        cleanupAndExitWith ExitSuccess
210
211
212
213

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

216
217
218
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
219
220
221
222
223
224
        cleanupAndExitWith $ ExitFailure 3

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