Skip to content

Commit

Permalink
SAPIC: translate processes by default (tamarin-prover#530)
Browse files Browse the repository at this point in the history
* Updated Stack to LTS 20-12 (GHC 9.2.6).

* Have translation into MSR rules be the default.

---------

Co-authored-by: Robert Künnemann <robert.kuennemann@cispa.saarland>
  • Loading branch information
rkunnema and Robert Künnemann committed Mar 30, 2023
1 parent 2106e17 commit d9eaa24
Showing 1 changed file with 2 additions and 5 deletions.
7 changes: 2 additions & 5 deletions src/Main/TheoryLoader.hs
Original file line number Diff line number Diff line change
Expand Up @@ -253,10 +253,8 @@ mkTheoryLoadOptions as = TheoryLoadOptions
autoSources = return $ argExists "auto-sources" as

outputModule
-- when proving, we act like we chose the Msr Output module.
| Nothing <- findArg "outModule" as , [] /= findArg "prove" as = return $ Just ModuleMsr
-- default
| Nothing <- findArg "outModule" as = return $ Just ModuleSpthy
-- MSR is default module, i.e., we translate by default ... otherwise we get warnings for actions used in lemmas that appear only in processes.
| Nothing <- findArg "outModule" as = return $ Just ModuleMsr
-- Otherwise, find output module that matches string argument
| Just str <- findArg "outModule" as
, Just modCon <- find (\x -> show x == str) (enumFrom minBound) = return $ Just modCon
Expand Down Expand Up @@ -337,7 +335,6 @@ loadTheory thyOpts input inFile = do
isDiffMode = L.get oDiffMode thyOpts
isMSRModule = L.get oOutputModule thyOpts == Just ModuleMsr


unwrapError (Left (Left e)) = Left e
unwrapError (Left (Right v)) = Right $ Left v
unwrapError (Right (Left e)) = Left e
Expand Down

0 comments on commit d9eaa24

Please sign in to comment.