Notice: If you are member of any public project or group, please make sure that your GitLab username is not the same as the LRZ identifier/Kennung (see https://gitlab.lrz.de/profile/account). Please change your username if necessary. For more information see the section "Public projects / Öffentliche Projekte" at https://doku.lrz.de/display/PUBLIC/GitLab . Thank you!

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

module Options
4
    (InputFormat(..),OutputFormat(..),RefinementType(..),RefinementOption(..),BackendSolver(..),
5
     PropertyOption(..),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)

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
data BackendSolver = Z3
                   | CVC4

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

32 33 34
data PropertyOption = PropDefault
                      | PropList [Property]

35 36 37 38
data RefinementOption = RefDefault
                      | RefList [RefinementType]
                      | RefAll

Philipp Meyer's avatar
Philipp Meyer committed
39 40 41 42
data Options = Options { inputFormat :: InputFormat
                       , optVerbosity :: Int
                       , optShowHelp :: Bool
                       , optShowVersion :: Bool
43
                       , optSolver :: BackendSolver
44
                       , optProperties :: PropertyOption
45
                       , optRefinementType :: RefinementOption
46
                       , optMinimizeRefinement :: Int
Philipp Meyer's avatar
Philipp Meyer committed
47 48 49 50 51 52 53 54
                       , optInvariant :: Bool
                       , optOutput :: Maybe String
                       , outputFormat :: OutputFormat
                       , optUseProperties :: Bool
                       , optPrintStructure :: Bool
                       }

startOptions :: Options
55
startOptions = Options { inputFormat = InPP
Philipp Meyer's avatar
Philipp Meyer committed
56 57 58
                       , optVerbosity = 1
                       , optShowHelp = False
                       , optShowVersion = False
59
                       , optSolver = Options.Z3
60
                       , optProperties = PropDefault
61
                       , optRefinementType = RefDefault
62
                       , optMinimizeRefinement = 0
Philipp Meyer's avatar
Philipp Meyer committed
63 64
                       , optInvariant = False
                       , optOutput = Nothing
65
                       , outputFormat = OutDOT
Philipp Meyer's avatar
Philipp Meyer committed
66 67 68 69
                       , optUseProperties = True
                       , optPrintStructure = False
                       }

70 71 72 73 74 75 76 77
addProperty :: Property -> Options -> Either String Options
addProperty prop opt =
        Right opt {
           optProperties = case optProperties opt of
                               PropDefault -> PropList [prop]
                               (PropList props) -> PropList (props ++ [prop])
       }

Philipp Meyer's avatar
Philipp Meyer committed
78 79
options :: [ OptDescr (Options -> Either String Options) ]
options =
80
        [ Option "" ["layered-termination"]
81
        (NoArg (addProperty LayeredTermination))
82
        "Prove that the protocol satisfies layered termination"
83

84
        , Option "" ["strong-consensus"]
85
        (NoArg (addProperty StrongConsensus))
86
        "Prove that the protocol satisfies strong consensus"
87

88
        , Option "" ["correctness"]
89
        (NoArg (addProperty StrongConsensusWithCorrectness))
90 91
        "Prove that the protocol correctly satisfies the given predicate"

92 93 94 95
        , Option "i" ["invariant"]
        (NoArg (\opt -> Right opt { optInvariant = True }))
        "Generate an invariant"

96 97 98 99 100 101 102 103 104 105
        , Option "" ["solver"]
        (ReqArg (\arg opt ->
            case arg of
                        "z3" -> Right opt { optSolver = Options.Z3 }
                        "cvc4" -> Right opt { optSolver = Options.CVC4 }
                        _ -> Left ("invalid argument for refinement method: " ++ arg)
                )
                "SOLVER")
        ("Use backend solver SOLVER (z3, cvc4)")

106
        , Option "r" ["refinement"]
107 108
        (ReqArg (\arg opt ->
                    let addRef ref =
109 110 111 112
                            case optRefinementType opt of
                               RefDefault -> RefList [ref]
                               (RefList refs) -> RefList (refs ++ [ref])
                               RefAll -> RefAll
113
                    in case arg of
114 115 116 117 118 119
                                "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 }
120
                                _ -> Left ("invalid argument for refinement method: " ++ arg)
121 122
                )
                "METHOD")
123
        ("Refine with METHOD (trap, siphon, utrap, usiphon, none, all)")
Philipp Meyer's avatar
Philipp Meyer committed
124

125
        , Option "s" ["structure"]
126 127 128 129 130 131
        (NoArg (\opt -> Right opt {
                                  optPrintStructure = True,
                                  optProperties = case optProperties opt of
                                                       PropDefault -> PropList []
                                                       (PropList props) -> PropList props
                        }))
132 133 134 135 136 137 138 139
        "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
140 141 142 143 144
        , Option "o" ["output"]
        (ReqArg (\arg opt -> Right opt {
                        optOutput = Just arg
                })
                "FILE")
145
        "Write population protocol to FILE"
Philipp Meyer's avatar
Philipp Meyer committed
146 147 148 149 150

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

151
        , Option "m" ["minimize"]
152 153 154
        (ReqArg (\arg opt -> case reads arg of
                        [(i, "")] -> Right opt { optMinimizeRefinement = i }
                        _ -> Left ("invalid argument for minimization method: " ++ arg)
155 156
                )
                "METHOD")
157 158
        "Minimize size of refinement structure by method METHOD (1-4)"

Philipp Meyer's avatar
Philipp Meyer committed
159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184
        , 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
185 186
usageInformation =
        usageInfo ("Usage: peregrine [OPTIONS] FILE\n") options