Main.hs 8.02 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 -> RefinementObjects ->
        OptIO (Maybe StrongConsensusCounterExample, RefinementObjects)
checkStrongConsensus' pp refinements = do
        r <- checkSat $ checkStrongConsensusSat pp refinements
104
        case r of
105
            Nothing -> return (Nothing, refinements)
106
            Just c -> do
107
108
109
110
111
112
                optRefine <- opt optRefinementType
                let refinementMethods = case optRefine of
                        RefDefault -> [TrapRefinement, SiphonRefinement, UTrapRefinement, USiphonRefinement]
                        RefList rs -> rs
                        RefAll -> error "not yet implemented"
                refineStrongConsensus pp refinementMethods refinements c
113

114
115
116
117
118
119
120
121
122
123
124
125
126

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
127
            Nothing -> do
128
129
130
131
132
133
134
135
136
                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'
137

Philipp Meyer's avatar
Philipp Meyer committed
138
139
checkLayeredTermination :: PopulationProtocol -> OptIO PropResult
checkLayeredTermination pp = do
140
        let nonTrivialTriplets = filter (not . trivialTriplet) $ generateTriplets pp
Philipp Meyer's avatar
Philipp Meyer committed
141
        checkLayeredTermination' pp nonTrivialTriplets 1 $ genericLength $ transitions pp
142

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

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

exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
182
        cleanupAndExitWith ExitSuccess
183
184
185
186

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

189
190
191
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
192
193
194
195
196
197
        cleanupAndExitWith $ ExitFailure 3

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