Options.hs 6.03 KB
Newer Older
Philipp Meyer's avatar
Philipp Meyer committed
1
2
3
{-# LANGUAGE TupleSections #-}

module Options
4
    (InputFormat(..),OutputFormat(..),RefinementType(..),RefinementOption(..),
Philipp Meyer's avatar
Philipp Meyer committed
5
     Options(..),startOptions,options,parseArgs,
Philipp Meyer's avatar
Philipp Meyer committed
6
7
8
9
10
11
12
     usageInformation)
where

import Control.Applicative ((<$>))
import System.Console.GetOpt
import System.Environment (getArgs)

Philipp Meyer's avatar
Philipp Meyer committed
13
14
import Property (Property(..))

15
16
data InputFormat = InPP deriving (Read)
data OutputFormat = OutDOT deriving (Read)
Philipp Meyer's avatar
Philipp Meyer committed
17

18
19
instance Show InputFormat where
        show InPP = "PP"
Philipp Meyer's avatar
Philipp Meyer committed
20
21
22
instance Show OutputFormat where
        show OutDOT = "DOT"

23
24
25
26
data RefinementType = TrapRefinement
                    | SiphonRefinement
                    | UTrapRefinement
                    | USiphonRefinement
27
28
                    deriving (Show,Read)

29
30
31
32
data RefinementOption = RefDefault
                      | RefList [RefinementType]
                      | RefAll

Philipp Meyer's avatar
Philipp Meyer committed
33
34
35
36
data Options = Options { inputFormat :: InputFormat
                       , optVerbosity :: Int
                       , optShowHelp :: Bool
                       , optShowVersion :: Bool
Philipp Meyer's avatar
Philipp Meyer committed
37
                       , optProperties :: [Property]
38
                       , optRefinementType :: RefinementOption
39
                       , optMinimizeRefinement :: Int
40
                       , optSMTAuto :: Bool
Philipp Meyer's avatar
Philipp Meyer committed
41
42
43
44
45
46
47
48
                       , optInvariant :: Bool
                       , optOutput :: Maybe String
                       , outputFormat :: OutputFormat
                       , optUseProperties :: Bool
                       , optPrintStructure :: Bool
                       }

startOptions :: Options
49
startOptions = Options { inputFormat = InPP
Philipp Meyer's avatar
Philipp Meyer committed
50
51
52
53
                       , optVerbosity = 1
                       , optShowHelp = False
                       , optShowVersion = False
                       , optProperties = []
54
                       , optRefinementType = RefDefault
55
                       , optMinimizeRefinement = 0
56
                       , optSMTAuto = True
Philipp Meyer's avatar
Philipp Meyer committed
57
58
                       , optInvariant = False
                       , optOutput = Nothing
59
                       , outputFormat = OutDOT
Philipp Meyer's avatar
Philipp Meyer committed
60
61
62
63
64
65
                       , optUseProperties = True
                       , optPrintStructure = False
                       }

options :: [ OptDescr (Options -> Either String Options) ]
options =
Philipp Meyer's avatar
Philipp Meyer committed
66
        [ Option "" ["layered-termination"]
67
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
68
                   optProperties = optProperties opt ++ [LayeredTermination]
69
               }))
Philipp Meyer's avatar
Philipp Meyer committed
70
        "Prove that the protocol satisfies layered termination"
71

Philipp Meyer's avatar
Philipp Meyer committed
72
        , Option "" ["strong-consensus"]
73
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
74
                   optProperties = optProperties opt ++ [StrongConsensus]
75
               }))
Philipp Meyer's avatar
Philipp Meyer committed
76
        "Prove that the protocol satisfies strong consensus"
77

78
79
80
81
        , Option "i" ["invariant"]
        (NoArg (\opt -> Right opt { optInvariant = True }))
        "Generate an invariant"

82
        , Option "r" ["refinement"]
83
84
        (ReqArg (\arg opt ->
                    let addRef ref =
85
86
87
88
                            case optRefinementType opt of
                               RefDefault -> RefList [ref]
                               (RefList refs) -> RefList (refs ++ [ref])
                               RefAll -> RefAll
89
                    in case arg of
90
91
92
93
94
95
                                "none" -> Right opt { optRefinementType = RefList [] }
                                "trap" -> Right opt { optRefinementType = addRef TrapRefinement }
                                "siphon" -> Right opt { optRefinementType = addRef SiphonRefinement }
                                "utrap" -> Right opt { optRefinementType = addRef UTrapRefinement }
                                "usiphon" -> Right opt { optRefinementType = addRef USiphonRefinement }
                                "all" -> Right opt { optRefinementType = RefAll }
96
                                _ -> Left ("invalid argument for refinement method: " ++ arg)
97
98
                )
                "METHOD")
99
        ("Refine with METHOD (trap, siphon, utrap, usiphon, none, all)")
Philipp Meyer's avatar
Philipp Meyer committed
100

Philipp Meyer's avatar
Philipp Meyer committed
101
102
103
104
105
106
107
108
109
110
        , Option "s" ["structure"]
        (NoArg (\opt -> Right opt { optPrintStructure = True }))
        "Print structural information"


        , Option "" ["in-pp"]
        (NoArg (\opt -> Right opt { inputFormat = InPP }))
        "Use the population protocol input format"


Philipp Meyer's avatar
Philipp Meyer committed
111
112
113
114
115
        , Option "o" ["output"]
        (ReqArg (\arg opt -> Right opt {
                        optOutput = Just arg
                })
                "FILE")
116
        "Write population protocol to FILE"
Philipp Meyer's avatar
Philipp Meyer committed
117
118
119
120
121

        , Option "" ["out-dot"]
        (NoArg (\opt -> Right opt { outputFormat = OutDOT }))
        "Use the dot output format"

122
        , Option "m" ["minimize"]
123
124
125
        (ReqArg (\arg opt -> case reads arg of
                        [(i, "")] -> Right opt { optMinimizeRefinement = i }
                        _ -> Left ("invalid argument for minimization method: " ++ arg)
126
127
                )
                "METHOD")
128
129
        "Minimize size of refinement structure by method METHOD (1-4)"

130
131
132
133
        , Option "" ["smt-disable-auto-config"]
        (NoArg (\opt -> Right opt { optSMTAuto = False }))
        "Disable automatic configuration of the SMT solver"

Philipp Meyer's avatar
Philipp Meyer committed
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
        , Option "v" ["verbose"]
        (NoArg (\opt -> Right opt { optVerbosity = optVerbosity opt + 1 }))
        "Increase verbosity (may be specified more than once)"

        , Option "q" ["quiet"]
        (NoArg (\opt -> Right opt { optVerbosity = optVerbosity opt - 1 }))
        "Decrease verbosity (may be specified more than once)"

        , Option "V" ["version"]
        (NoArg (\opt -> Right opt { optShowVersion = True }))
        "Show version"

        , Option "h" ["help"]
        (NoArg (\opt -> Right opt { optShowHelp = True }))
        "Show help"
        ]

parseArgs :: IO (Either String (Options, [String]))
parseArgs = do
        args <- getArgs
        case getOpt Permute options args of
            (actions, files, []) ->
                return $ (,files) <$> foldl (>>=) (return startOptions) actions
            (_, _, errs) -> return $ Left $ concat errs

usageInformation :: String
Philipp Meyer's avatar
Philipp Meyer committed
160
161
usageInformation =
        usageInfo ("Usage: peregrine [OPTIONS] FILE\n") options