Main.hs 8.43 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
41
42
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))
        verbosePut 0 $ "Yes states         : " ++ show (length (yesStates pp))
        verbosePut 0 $ "No states          : " ++ show (length (noStates 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
printInvariant :: (Show a, Invariant a) => (Maybe [a], [a]) -> OptIO PropResult
printInvariant (baseInvResult, addedInv) =
        case baseInvResult of
Philipp Meyer's avatar
Philipp Meyer committed
88
            Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
89
                verbosePut 0 "No invariant found"
Philipp Meyer's avatar
Philipp Meyer committed
90
                return Unknown
91
            Just baseInv -> do
Philipp Meyer's avatar
Philipp Meyer committed
92
                verbosePut 0 "Invariant found"
93
94
95
                let baseSize = map invariantSize baseInv
                let addedSize = map invariantSize addedInv
                verbosePut 2 $ "Number of atoms in base invariants: " ++ show baseSize ++
96
                        " (total of " ++ show (sum baseSize) ++ ")"
97
                verbosePut 2 $ "Number of atoms in added invariants: " ++ show addedSize ++
98
                        " (total of " ++ show (sum addedSize) ++ ")"
99
100
                mapM_ (putLine . show) baseInv
                mapM_ (putLine . show) addedInv
Philipp Meyer's avatar
Philipp Meyer committed
101
102
                return Satisfied

Philipp Meyer's avatar
Philipp Meyer committed
103
104
105
checkStrongConsensus :: PopulationProtocol -> OptIO PropResult
checkStrongConsensus pp = do
        r <- checkStrongConsensus' pp [] [] []
106
        case r of
107
108
            (Nothing, _, _, _) -> return Satisfied
            (Just _, _, _, _) -> return Unknown
109

Philipp Meyer's avatar
Philipp Meyer committed
110
checkStrongConsensus' :: PopulationProtocol ->
111
        [Trap] -> [Siphon] -> [StableInequality] ->
Philipp Meyer's avatar
Philipp Meyer committed
112
113
114
        OptIO (Maybe StrongConsensusCounterExample, [Trap], [Siphon], [StableInequality])
checkStrongConsensus' pp utraps usiphons inequalities = do
        r <- checkSat $ checkStrongConsensusSat pp utraps usiphons inequalities
115
        case r of
116
            Nothing -> return (Nothing, utraps, usiphons, inequalities)
117
            Just c -> do
118
119
                refine <- opt optRefinementType
                if isJust refine then
Philipp Meyer's avatar
Philipp Meyer committed
120
                    refineStrongConsensus pp utraps usiphons inequalities c
121
                else
122
                    return (Just c, utraps, usiphons, inequalities)
123

Philipp Meyer's avatar
Philipp Meyer committed
124
125
126
127
128
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
129
130
        case r1 of
            Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
131
                r2 <- checkSatMin $ Solver.StrongConsensus.findUSiphonConstraintsSat pp m0 m1 m2 x1 x2
132
133
                case r2 of
                    Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
134
                        r3 <- checkSatMin $ Solver.StrongConsensus.findUTrapConstraintsSat pp m0 m1 m2 x1 x2
Philipp J. Meyer's avatar
Philipp J. Meyer committed
135
                        case r3 of
136
                            Nothing -> return (Just c, utraps, usiphons, inequalities)
Philipp J. Meyer's avatar
Philipp J. Meyer committed
137
                            Just utrap ->
Philipp Meyer's avatar
Philipp Meyer committed
138
                                checkStrongConsensus' pp (utrap:utraps) usiphons inequalities
Philipp J. Meyer's avatar
Philipp J. Meyer committed
139
                    Just usiphon ->
Philipp Meyer's avatar
Philipp Meyer committed
140
                        checkStrongConsensus' pp utraps (usiphon:usiphons) inequalities
141
            Just trap ->
Philipp Meyer's avatar
Philipp Meyer committed
142
                checkStrongConsensus' pp (trap:utraps) usiphons inequalities
143

Philipp Meyer's avatar
Philipp Meyer committed
144
145
checkLayeredTermination :: PopulationProtocol -> OptIO PropResult
checkLayeredTermination pp = do
146
        let nonTrivialTriplets = filter (not . trivialTriplet) $ generateTriplets pp
Philipp Meyer's avatar
Philipp Meyer committed
147
        checkLayeredTermination' pp nonTrivialTriplets 1 $ genericLength $ transitions pp
148

Philipp Meyer's avatar
Philipp Meyer committed
149
150
checkLayeredTermination' :: PopulationProtocol -> [Triplet] -> Integer -> Integer -> OptIO PropResult
checkLayeredTermination' pp triplets k kmax = do
151
        verbosePut 1 $ "Checking terminal marking reachable with at most " ++ show k ++ " partitions"
Philipp Meyer's avatar
Philipp Meyer committed
152
        r <- checkSatMin $ checkLayeredTerminationSat pp triplets k
153
        case r of
154
155
            Nothing ->
                if k < kmax then
Philipp Meyer's avatar
Philipp Meyer committed
156
                    checkLayeredTermination' pp triplets (k + 1) kmax
157
158
                else
                    return Unknown
159
160
161
162
163
164
165
            Just inv -> do
                invariant <- opt optInvariant
                if invariant then
                    printInvariant (Just inv, [])
                else
                    return Satisfied

166
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
167
main = do
Philipp Meyer's avatar
Philipp Meyer committed
168
        putStrLn "Peregrine - Efficient Verification of Population Protocols\n"
169
170
171
172
173
        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
174
                when (optShowHelp opts) (exitSuccessWith usageInformation)
175
                when (null files) (exitErrorWith "No input file given")
176
                let opts' = opts { optProperties = reverse (optProperties opts) }
Philipp Meyer's avatar
Philipp Meyer committed
177
                rs <- runReaderT (mapM checkFile files) opts'
178
179
                -- TODO: short-circuit with Control.Monad.Loops? parallel
                -- execution?
Philipp Meyer's avatar
Philipp Meyer committed
180
181
                let r = resultsAnd rs
                case r of
182
                    Satisfied ->
Philipp Meyer's avatar
Philipp Meyer committed
183
184
185
                        exitSuccessWith $ "All properties " ++ show r
                    _ ->
                        exitFailureWith $ "Some properties " ++ show r
186
187
188
189

exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
190
        cleanupAndExitWith ExitSuccess
191
192
193
194

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

197
198
199
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
200
201
202
203
204
205
        cleanupAndExitWith $ ExitFailure 3

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