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

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

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

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

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

21
data ImplicitProperty = TerminalMarkingsUniqueConsensus
22
                      | TerminalMarkingReachable
Philipp Meyer's avatar
Philipp Meyer committed
23
24
                      deriving (Show,Read)

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

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

startOptions :: Options
48
startOptions = Options { inputFormat = InPP
Philipp Meyer's avatar
Philipp Meyer committed
49
50
51
52
                       , optVerbosity = 1
                       , optShowHelp = False
                       , optShowVersion = False
                       , optProperties = []
53
                       , optRefinementType = Just [TrapRefinement, SiphonRefinement, UTrapRefinement, USiphonRefinement]
54
                       , optMinimizeRefinement = 0
55
                       , optSMTAuto = True
Philipp Meyer's avatar
Philipp Meyer committed
56
                       , optInvariant = False
57
                       , optBoolConst = False
Philipp Meyer's avatar
Philipp Meyer committed
58
                       , 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 =
66
67
68
        [ Option "" ["pp"]
        (NoArg (\opt -> Right opt { inputFormat = InPP }))
        "Use the population protocol input format"
Philipp Meyer's avatar
Philipp Meyer committed
69

70
        , Option "" ["structure"]
Philipp Meyer's avatar
Philipp Meyer committed
71
72
73
        (NoArg (\opt -> Right opt { optPrintStructure = True }))
        "Print structural information"

74
        , Option "" ["terminal-markings-unique-consensus"]
75
        (NoArg (\opt -> Right opt {
76
                   optProperties = optProperties opt ++ [TerminalMarkingsUniqueConsensus]
77
               }))
78
        "Prove that terminal markings have a unique consensus"
79

80
81
        , Option "" ["terminal-marking-reachable"]
        (NoArg (\opt -> Right opt {
82
                   optProperties = optProperties opt ++ [TerminalMarkingReachable]
83
84
85
               }))
        "Prove that a terminal marking is reachable"

86
87
88
89
        , Option "i" ["invariant"]
        (NoArg (\opt -> Right opt { optInvariant = True }))
        "Generate an invariant"

90
91
92
93
94
        , Option "" ["bool-const"]
        (NoArg (\opt -> Right opt { optBoolConst = True }))
        ("Use boolean constraints instead of integer ones\n" ++
         "  for transition invariant")

95
        , Option "r" ["refinement"]
96
97
98
99
100
101
102
103
104
105
106
107
108
109
        (ReqArg (\arg opt ->
                    let addRef ref =
                            Right opt { optRefinementType =
                                    case optRefinementType opt of
                                       Nothing -> Just [ref]
                                       Just(refs) -> Just (refs ++ [ref])

                            }
                    in case arg of
                                "trap" -> addRef TrapRefinement
                                "siphon" -> addRef SiphonRefinement
                                "utrap" -> addRef UTrapRefinement
                                "usiphon" -> addRef USiphonRefinement
                                _ -> Left ("invalid argument for refinement method: " ++ arg)
110
111
                )
                "METHOD")
112
        ("Refine with METHOD (trap, siphon, utrap, usiphon)")
Philipp Meyer's avatar
Philipp Meyer committed
113
114
115
116
117
118

        , Option "o" ["output"]
        (ReqArg (\arg opt -> Right opt {
                        optOutput = Just arg
                })
                "FILE")
119
        "Write population protocol to FILE"
Philipp Meyer's avatar
Philipp Meyer committed
120
121
122
123
124

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

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

133
134
135
136
        , 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
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
        , 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
163
usageInformation = usageInfo "Peregrine" options