diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,7 @@ -# Revision history for flint-simulation +# Revision history for package `eflint` -## 0.1.0.0 -- YYYY-mm-dd +## 3.1.0.0 (2023/05/22) -* First version. Released on an unsuspecting world. +* Started using changelog. + +Last significant update: inclusion of 'instance queries' of the form `?- .` diff --git a/eflint.cabal b/eflint.cabal --- a/eflint.cabal +++ b/eflint.cabal @@ -1,7 +1,7 @@ cabal-version: >=1.10 name: eflint -version: 3.0.0.2 +version: 3.1.0.0 synopsis: Simulation interpreter for FLINT policy descriptions description: @@ -42,11 +42,11 @@ Language.EFLINT.Interpreter Language.EFLINT.Util Language.EFLINT.Options - build-depends: base >=4.9 && < 4.15 + build-depends: base >=4.9 && < 5 , containers >=0.5 && <0.7 , hxt >= 9.3.1.16 , time >= 1.8.0.2 - , gll >= 0.4.0.13 + , gll >= 0.4.1.0 , regex-applicative >= 0.3.3 , aeson >= 1.4.6.0 , bytestring >= 0.10.8.2 @@ -54,7 +54,7 @@ , text >= 1.2.4.0 , filepath >= 1.4.2 , directory >= 1.3.6 - , exploring-interpreters >= 1.3.0.0 + , exploring-interpreters >= 1.4.0.0 , fgl >= 5.7 , mtl >= 2.2 hs-source-dirs: src @@ -76,11 +76,11 @@ Language.EFLINT.Interpreter Language.EFLINT.Util Language.EFLINT.Options - build-depends: base >=4.9 && < 4.15 + build-depends: base >=4.9 && < 5 , containers >=0.5 && <0.7 , hxt >= 9.3.1.16 , time >= 1.8.0.2 - , gll >= 0.4.0.13 + , gll >= 0.4.1.0 , regex-applicative >= 0.3.3 , aeson >= 1.4.6.0 , bytestring >= 0.10.8.2 @@ -90,7 +90,7 @@ , mtl >= 2.2 , haskeline >= 0.8.1 , transformers >= 0.5.6 - , exploring-interpreters >= 1.3.0.0 + , exploring-interpreters >= 1.4.0.0 , text hs-source-dirs: src default-language: Haskell2010 @@ -111,18 +111,18 @@ Language.EFLINT.JSON Language.EFLINT.Util Language.EFLINT.Options - build-depends: base >=4.9 && < 4.15 + build-depends: base >=4.9 && < 5 , containers >=0.5 && <0.7 , hxt >= 9.3.1.16 , time >= 1.8.0.2 - , gll >= 0.4.0.13 + , gll >= 0.4.1.0 , regex-applicative >= 0.3.3 , aeson >= 1.4.6.0 , bytestring >= 0.10.8.2 , network >= 3.1 , filepath >= 1.4.2 , directory >= 1.3.6 - , exploring-interpreters >= 1.3.0.0 + , exploring-interpreters >= 1.4.0.0 , fgl >= 5.7 , mtl >= 2.2 hs-source-dirs: src diff --git a/src/Language/EFLINT/Eval.hs b/src/Language/EFLINT/Eval.hs --- a/src/Language/EFLINT/Eval.hs +++ b/src/Language/EFLINT/Eval.hs @@ -12,6 +12,7 @@ import Data.List ((\\)) import Data.Maybe (fromJust) import qualified Data.Map as M +import qualified Data.Set as S data M_Subs a = M_Subs { runSubs :: Spec -> State -> InputMap -> Subs -> Either RuntimeError [a] } @@ -248,20 +249,26 @@ (ass `store_union` ass', is_f || is_f') instantiate_trans :: Tagged -> M_Subs TransInfo -instantiate_trans te@(v,d) = do +instantiate_trans = instantiate_trans' S.empty + +instantiate_trans' :: S.Set Tagged -> Tagged -> M_Subs TransInfo +instantiate_trans' done' te@(v,d) + | te `S.member` done' = empty + | otherwise = do tspec <- get_type_spec d is_enabled <- is_enabled te case kind tspec of Fact _ -> empty Duty _ -> empty Act aspec -> do_transition te actor is_enabled (effects aspec) (syncs aspec) - Event espec -> do_transition te Nothing is_enabled (event_effects espec) [] - where do_transition te@(v,d) mActor is_enabled effects ss = do + Event espec -> do_transition te Nothing is_enabled (event_effects espec) (event_syncs espec) + where done = te `S.insert` done' + do_transition te@(v,d) mActor is_enabled effects ss = do (dom, _) <- get_dom d let Products xs = dom let Product args = v modify_subs (`subsUnion` (M.fromList (zip xs args))) $ do - sync_infos <- concat <$> mapM eval_sync ss + sync_infos <- concat <$> mapM (eval_sync' done) ss let (ss_ass,any_f) = syncTransInfos sync_infos ass' <- store_unions <$> mapM eval_effect effects let ass = ass' `store_union` ss_ass @@ -270,7 +277,10 @@ _ -> Nothing eval_sync :: Sync -> M_Subs [TransInfo] -eval_sync (Sync xs t) = foreach xs (whenTagged (eval t) instantiate_trans) +eval_sync = eval_sync' S.empty + +eval_sync' :: S.Set Tagged -> Sync -> M_Subs [TransInfo] +eval_sync' done (Sync xs t) = foreach xs (whenTagged (eval t) (instantiate_trans' done)) eval_effect :: Effect -> M_Subs Store eval_effect (CAll xs t) = M.fromList . map (,HoldsTrue) <$> foreach xs (whenTagged (eval t) return) diff --git a/src/Language/EFLINT/Explorer.hs b/src/Language/EFLINT/Explorer.hs --- a/src/Language/EFLINT/Explorer.hs +++ b/src/Language/EFLINT/Explorer.hs @@ -8,7 +8,7 @@ import Language.EFLINT.Print() import qualified Language.Explorer.Pure as EI -import Language.Explorer.Monadic (jump) +import Language.Explorer.Monadic (revert, jump) import Data.Tree (drawTree, Tree(..)) @@ -18,7 +18,7 @@ data Instruction = Execute [Program] InputMap | ExecuteOnce Program InputMap - | Revert Ref + | Revert Ref Bool {- whether the revert is destructive or not -} | Display Ref -- `last' edge leading to given ref | DisplayFull Ref -- full `history', see `Path' below, for given ref | ExplorationHeads -- nodes in the execution graph without outgoing edges @@ -100,7 +100,7 @@ cfg' = EI.config exp' ref' = EI.currRef exp' in ResultTrans exp' outs (EI.config exp, EI.currRef exp) (cfg', ref') - Revert r -> case jump r exp of + Revert r d -> case (if d then revert else jump) r exp of Nothing -> InvalidRevert Just exp' -> ResultTrans exp' [] (EI.config exp, EI.currRef exp) (EI.config exp', EI.currRef exp') Display id -> ResultTrans exp out (from, pr) (to, cr) diff --git a/src/Language/EFLINT/Interpreter.hs b/src/Language/EFLINT/Interpreter.hs --- a/src/Language/EFLINT/Interpreter.hs +++ b/src/Language/EFLINT/Interpreter.hs @@ -2,7 +2,7 @@ module Language.EFLINT.Interpreter (Config(..), Program(..), interpreter, initialConfig, rest_disabled, rest_enabled, get_transition, context2config, make_initial_state ,OutputWriter, Output(..), getOutput - ,errors, violations, ex_triggers, query_ress, missing_inputs + ,errors, violations, ex_triggers, query_ress, inst_query_ress, missing_inputs ,convert_programs, collapse_programs) where import Language.EFLINT.Eval @@ -34,7 +34,8 @@ data Output = ErrorVal Error | ExecutedTransition TransInfo | Violation Violation - | QueryRes QueryRes -- whether query succeed or not + | QueryRes QueryRes -- whether query succeed or not + | InstQueryRes [Tagged] deriving (Eq, Show, Read) convert_programs :: [Phrase] -> [Program] @@ -99,6 +100,11 @@ where op (QueryRes b) = [b] op _ = [] +inst_query_ress :: [Output] -> [[Tagged]] +inst_query_ress = concatMap op + where op (InstQueryRes vs) = [vs] + op _ = [] + missing_inputs :: [Output] -> [Tagged] missing_inputs = S.toList . S.fromList . concatMap op where op (ErrorVal (RuntimeError (MissingInput te))) = [te] @@ -122,6 +128,8 @@ let queryRes | all (== (ResBool True)) vs = QuerySuccess | otherwise = QueryFailure tell [QueryRes queryRes] >> no_effect + CInstQuery vs t -> error_or_process (foreach vs (whenTagged (eval (When t (Present t))) return)) spec state inpm $ \vs -> + do tell [InstQueryRes (concat vs)] >> no_effect CCreate vs t -> single_effect (CAll vs t) CTerminate vs t -> single_effect (TAll vs t) CObfuscate vs t -> single_effect (OAll vs t) @@ -152,7 +160,7 @@ , ctx_transitions = concat tss , ctx_duties = duties } - where state' = rebase_and_sat spec (make_assignments ass state) + where state' = rebase_and_sat spec (make_assignments spec' ass state) spec' = process_directives dirs spec no_effect :: OutputWriter (Maybe Context) @@ -170,11 +178,20 @@ consider_transinfos [Left d] = tell [ErrorVal (NotTriggerable d)] >> no_effect consider_transinfos [Right infos] = do forM_ infos $ \info -> do tell [ExecutedTransition info] - when (trans_is_action info && trans_forced info) - (tell [Violation (TriggerViolation info)]) + tell_violations info return_context (store_unions (map trans_assignments infos)) [] consider_transinfos _ = error "ASSERT: consider_transinfos" +tell_violations :: TransInfo -> OutputWriter () +tell_violations info + | trans_is_action info = + -- report whether this action is violated (potentially caused by any successor) + -- if not violated, then so will not any successor + when (trans_forced info) (tell [Violation (TriggerViolation info)]) + | otherwise = + -- report whether successors are violated, given that they could be actions + mapM_ tell_violations (trans_syncs info) + find_inv_violations :: [DomId] -> M_Subs [Violation] find_inv_violations ds = do spec <- get_spec @@ -232,5 +249,5 @@ Left err -> error (print_runtime_error err) Right res -> case res of [] -> error "failed to initialise state" - [sto] -> rebase_and_sat spec (make_assignments sto emptyState) + [sto] -> rebase_and_sat spec (make_assignments spec sto emptyState) _ -> error "non-deterministic state initialisation" diff --git a/src/Language/EFLINT/JSON.hs b/src/Language/EFLINT/JSON.hs --- a/src/Language/EFLINT/JSON.hs +++ b/src/Language/EFLINT/JSON.hs @@ -30,6 +30,7 @@ kind = Spec.Act aspec , domain = Products args , domain_constraint = BoolLit True + , restriction = Nothing , derivation = [HoldsWhen condition_term] , closed = True , conditions = [] @@ -42,7 +43,8 @@ args = [no_decoration (actor a), no_decoration (interested_party a)] ++ objects aspec = ActSpec { effects = map mkT ((terminate :: Act -> [OptBinder]) a) ++ map mkC ((create :: Act -> [OptBinder]) a) - , syncs = [] } + , syncs = [] + , physical = False } where mkT ob = case ob of ImplicitDV expr -> tAll [] expr ExplicitDV b -> tAll (vars b) (binder_expression b) where tAll vs expr = TAll (map tVariable vs) (tExpr expr) @@ -59,6 +61,7 @@ , domain = Products $ [no_decoration (duty_holder d) ,no_decoration (claimant d)] ++ objects , domain_constraint = BoolLit True + , restriction = Nothing , derivation = case (derivation :: Duty -> Maybe Binder) d of Nothing -> [] Just b -> [dv (duty d) (vars b) (binder_expression b)] @@ -66,7 +69,9 @@ , conditions = [] } where dspec = DutySpec {enforcing_acts = maybe [] (:[]) (enforcing d) - ,violated_when = []} + ,violated_when = [] + ,terminating_acts = [] + ,creating_acts = []} objects | all isSpace (duty_components d) = [] | otherwise = [no_decoration (duty_components d)] @@ -79,6 +84,7 @@ _ -> Products [] Just dom -> tDomain dom , domain_constraint = BoolLit True + , restriction = Nothing , derivation = case function f of ImplicitDV expr -> case expr of RefExpr (BaseVar "[]") -> [] --Just (Dv [] (When (App (fact f) (Right [])) (BoolLit True))) diff --git a/src/Language/EFLINT/Options.hs b/src/Language/EFLINT/Options.hs --- a/src/Language/EFLINT/Options.hs +++ b/src/Language/EFLINT/Options.hs @@ -110,28 +110,12 @@ "n" -> False _ -> False -verbosity :: Options -> Int -> IO () -> IO () -verbosity opts loc m = do +verbosity :: Options -> Level -> IO () -> IO () +verbosity opts loc_level m = do limit <- limitM <$> readIORef opts - when (level <= limit) m + when (loc_level <= limit) m where limitM opts | debug opts = Verbose | test_mode opts = TestMode | otherwise = Default - level = case loc of - 0 -> Default - 1 -> Default - 2 -> Default - 3 -> TestMode - 4 -> TestMode - 5 -> TestMode - 6 -> Default - 7 -> Default - 8 -> Default - 9 -> Default - 10-> Default - 11-> Default - 12-> TestMode - _ -> Default - data Level = TestMode | Default | Verbose deriving (Ord, Enum, Eq) diff --git a/src/Language/EFLINT/Parse.hs b/src/Language/EFLINT/Parse.hs --- a/src/Language/EFLINT/Parse.hs +++ b/src/Language/EFLINT/Parse.hs @@ -19,8 +19,8 @@ , keywords = ["!?","||", "&&", "<=", ">=", "..", "True", "False", "Sum", "==", "!=", "When", "Where","Holds when", "Holds", "Present when", "Present", "Max", "Min", "Count", "Union", "Enabled", "Violated when", "Violated" , "Atom", "String", "Int", "Time", "Current Time" , "Exists", "Forall", "Foreach", "Force" - , "Extend", "Event", "Act", "Fact", "Invariant", "Predicate", "Duty", "Actor", "Holder", "Claimant", "Recipient", "Related to", "Conditioned by", "Creates", "Terminates", "Obfuscates", "Terminated by", "With" , "Identified by", "Derived from", "Derived externally", "Enforced by", "Syncs with" - , "Do", "Placeholder", "For", "Not", "Open", "Closed" + , "Extend", "Event", "Act", "Fact", "Physical", "Bool", "Var", "Function", "Invariant", "Predicate", "Duty", "Actor", "Holder", "Claimant", "Recipient", "Related to", "Conditioned by", "Creates", "Terminates", "Obfuscates", "Terminated by", "Created by", "With" , "Identified by", "Derived from", "Derived externally", "Enforced by", "Syncs with" + , "Do", "Placeholder", "For", "Not", "Open", "Closed", "?-" , "#", "##", "###", "####" , "#include", "#require" ] @@ -146,52 +146,74 @@ parse_flint = parse_component flint declarations :: BNF Token [Decl] -declarations = "declarations" <:=> multiple1 frame +declarations = "declarations" <:=> concat <$$> multiple1 frame placeholder :: BNF Token Decl placeholder = "placeholder-decl" <:=> PlaceholderDecl <$$ keyword "Placeholder" <**> id_lit <** keyword "For" <**> id_lit -frame :: BNF Token Decl +frame :: BNF Token [Decl] frame = "frame" <:=> fact <||> duty - <||> act + <||> act + <||> physical <||> event - <||> syn_ext - <||> placeholder + <||> (:[]) <$$> syn_ext + <||> (:[]) <$$> placeholder where fact = syn_fact_decl (make_fact False False) - <||> syn_actor_decl (make_fact False True) + <||> syn_bool_fact_decl make_bool_fact + <||> syn_actor_decl (\d -> make_fact False True d Nothing) <||> syn_pred_decl (make_pred False) <||> syn_inv_decl make_inv - where make_fact inv is_actor is_closed ty dom dom_filter clauses = - TypeDecl ty $ apply_type_ext ty clauses tspec + where make_fact :: Bool -> Bool -> Bool -> Maybe Restriction -> DomId -> Domain -> Term -> [ModClause] -> [Decl] + make_fact inv is_actor is_closed restr ty dom dom_filter clauses = + [TypeDecl ty tspec, TypeExt ty clauses] where tspec = TypeSpec { kind = Fact (FactSpec inv is_actor) , domain = dom , domain_constraint = dom_filter + , restriction = restr , derivation = [] , closed = is_closed , conditions = [] } - make_pred inv ty t = make_fact inv False True ty (Products []) (BoolLit True) [DerivationCl [HoldsWhen t]] + make_pred inv ty t = make_fact inv False True Nothing ty (Products []) (BoolLit True) [DerivationCl [HoldsWhen t]] make_inv ty t = make_pred True ty t + make_bool_fact is_closed ty clauses = + make_fact False False is_closed Nothing ty (Products []) (BoolLit True) clauses act = syn_act_decl make_act where make_act is_closed ty mact mrec attrs dom_filter clauses = - TypeDecl ty $ apply_type_ext ty clauses tspec + [TypeDecl ty tspec, TypeExt ty clauses] where tspec = TypeSpec { - kind = Act (ActSpec {effects = [], syncs = []} ), + kind = Act (ActSpec {effects = [], syncs = [], physical = False } ), domain = Products (actor:(maybe [] (:[]) mrec ++ attrs)), domain_constraint = dom_filter, + restriction = Nothing, derivation = [], closed = is_closed, conditions = [] } actor = maybe (no_decoration "actor") id mact + physical = syn_physical_decl make_physical + where make_physical ty mact attrs dom_filter clauses = + [TypeDecl ty tspec, TypeExt ty (holds_true:clauses)] + where tspec = TypeSpec { + kind = Act (ActSpec { effects = [], syncs = [], physical = True }), + domain = Products (actor:attrs), + domain_constraint = dom_filter, + restriction = Nothing, + derivation = [], + closed = True, + conditions = [] } + actor = maybe (no_decoration "actor") id mact + holds_true = DerivationCl [HoldsWhen (BoolLit True)] + event = syn_event_decl make_event where make_event is_closed ty attrs dom_filter clauses = - TypeDecl ty $ apply_type_ext ty clauses tspec + [TypeDecl ty tspec, TypeExt ty clauses] where tspec = TypeSpec { - kind = Event (EventSpec { event_effects = [] }) + kind = Event (EventSpec { event_effects = [], event_syncs = [] }) , domain = Products attrs , domain_constraint = dom_filter + , restriction = Nothing , derivation = [] , closed = is_closed , conditions = [] @@ -199,22 +221,34 @@ duty = syn_duty_decl make_duty where make_duty is_closed ty hold claim attrs dom_filter clauses = - TypeDecl ty $ apply_type_ext ty clauses tspec + [TypeDecl ty tspec, TypeExt ty clauses] where tspec = TypeSpec { domain = Products (hold:claim:attrs), domain_constraint = dom_filter, - kind = Duty (DutySpec { violated_when = [], enforcing_acts = []}), + restriction = Nothing, + kind = Duty (DutySpec { violated_when = [], enforcing_acts = [] + , terminating_acts = [], creating_acts = [] }), derivation = [], closed = is_closed, conditions = []} -syn_fact_decl :: (Bool -> DomId -> Domain -> Term -> [ModClause] -> a) -> BNF Token a +syn_fact_decl :: (Bool -> Maybe Restriction -> DomId -> Domain -> Term -> [ModClause] -> a) -> BNF Token a syn_fact_decl cons = "fact-type-decl" <:=> cons <$$> - syn_is_closed <** keyword "Fact" <**> id_lit <**> + syn_is_closed <**> fact_restriction_by_keyword <**> id_lit <**> optionalWithDef (keyword "Identified by" **> type_expr) AnyString <**> syn_domain_constraint <**> syn_fact_clauses +fact_restriction_by_keyword :: BNF Token (Maybe Restriction) +fact_restriction_by_keyword = "restricted-fact" <:=> + Nothing <$$ keyword "Fact" + <||> Just VarRestriction <$$ keyword "Var" + <||> Just FunctionRestriction <$$ keyword "Function" + +syn_bool_fact_decl :: (Bool -> DomId -> [ModClause] -> a) -> BNF Token a +syn_bool_fact_decl cons = "bool-fact-type-decl" <:=> cons <$$> + syn_is_closed <** keyword "Bool" <**> id_lit <**> syn_fact_clauses + syn_ext :: BNF Token Decl syn_ext = "type-ext" <:=> keyword "Extend" **> ( syn_fact_ext @@ -264,9 +298,18 @@ objects <**> syn_domain_constraint <**> syn_event_clauses +syn_physical_decl :: (DomId -> Maybe Var -> [Var] -> Term -> [ModClause] -> a) -> BNF Token a +syn_physical_decl cons = "physical-type-decl" <:=> cons <$$ + keyword "Physical" <**> id_lit <** optional (keyword "With") <**> + optional (keyword "Actor" **> var) <**> + objects <**> syn_domain_constraint <**> + syn_event_clauses + syn_act_ext :: BNF Token Decl syn_act_ext = "act-type-ext" <:=> TypeExt <$$ keyword "Act" <**> id_lit <**> syn_event_clauses +syn_physical_ext = "physical-type-ext" <:=> TypeExt <$$ keyword "Physical" <**> id_lit <**> syn_physical_clauses + syn_event_ext :: BNF Token Decl syn_event_ext = "event-type-ext" <:=> TypeExt <$$ keyword "Event" <**> id_lit <**> syn_event_clauses @@ -283,6 +326,14 @@ syn_fact_clauses = multiple syn_fact_clause where syn_fact_clause = "fact-clause" <:=> ConditionedByCl <$$> precondition' <||> DerivationCl <$$> derivation_from + +syn_physical_clauses :: BNF Token [ModClause] +syn_physical_clauses = multiple syn_physical_clause + where syn_physical_clause = "physical-clause" <:=> ConditionedByCl <$$> precondition' + <||> PostCondCl <$$> creating_post' + <||> PostCondCl <$$> terminating_post' + <||> PostCondCl <$$> obfuscating_post' + <||> SyncCl <$$> synchronisations syn_event_clauses :: BNF Token [ModClause] syn_event_clauses = multiple syn_event_clause @@ -299,6 +350,8 @@ <||> DerivationCl <$$> derivation_from <||> ViolationCl <$$> violation_condition <||> EnforcingActsCl <$$> enforcing_acts_clauses + <||> TerminatedByCl <$$> terminated_by_clauses + <||> CreatedByCl <$$> created_by_clauses objects :: BNF Token [Var] objects = "related-to" <:=> optionalWithDef (keyword "Related to" **> multipleSepBy1 var (keychar ',')) [] @@ -307,6 +360,14 @@ enforcing_acts_clauses = "enforcing-act-clauses" <:=> keyword "Enforced by" **> multipleSepBy1 id_lit (keychar ',') +terminated_by_clauses :: BNF Token [DomId] +terminated_by_clauses = "terminated-by-clauses" + <:=> keyword "Terminated by" **> multipleSepBy1 id_lit (keychar ',') + +created_by_clauses :: BNF Token [DomId] +created_by_clauses = "created-by-clauses" + <:=> keyword "Created by" **> multipleSepBy1 id_lit (keychar ',') + violation_condition :: BNF Token [Term] violation_condition = "violation-conditions" <:=> keyword "Violated when" **> multipleSepBy1 value_expr (keychar ',') @@ -392,17 +453,10 @@ <:=> foreach CAll <||> CAll [] <$$> value_expr --- parsing scenario specifications -parse_scenario :: String -> Either String Scenario -parse_scenario = parse_component scenario - + scenario :: BNF Token Scenario scenario = "scenario" <:=> multiple statement - -parse_statement :: String -> Either String Statement -parse_statement = parse_component statement - statement :: BNF Token Statement statement = "statement" <:=> ($) <$$> actioner <**> maybe_action <** keychar '.' @@ -416,19 +470,6 @@ <:=> application ([],,) <||> parens ((\xs (d,args) -> (xs,d,args)) <$$ keyword "Foreach" <**> (multipleSepBy1 var (keychar ',')) <** keychar ':' <**> application (,)) -statement_phrase :: BNF Token Phrase -statement_phrase = "statement-phrase" - <:=> ($) <$$> actioner <**> maybe_action <** keychar '.' - <||> PQuery <$$ keychar '?' <**> value_expr <** keychar '.' - <||> PQuery . Not <$$ keyword "!?" <**> value_expr <** keychar '.' - where actioner = "actioner" - <:=> (\(xs, d, ms) -> PTrigger xs (App d ms)) <$$ optional (keychar '!') - <||> (\(xs, d, ms) -> Create xs (App d ms)) <$$ keychar '+' - <||> (\(xs, d, ms) -> Terminate xs (App d ms)) <$$ keychar '-' - maybe_action = "action-statement" - <:=> application ([],,) - <||> parens ((\xs (d,args) -> (xs,d,args)) <$$ keyword "Foreach" <**> (multipleSepBy1 var (keychar ',')) <** keychar ':' <**> application (,)) - phrase_scenario :: BNF Token [Phrase] phrase_scenario = "phrase-scenario" <:=> multiple (syn_phrase <** keychar '.') @@ -453,6 +494,7 @@ <||> keychar '-' **> opt_foreach Terminate <||> keychar '~' **> opt_foreach Obfuscate <||> PQuery <$$ keychar '?' <**> value_expr - <||> PQuery . Not <$$ keyword "!?" <**> value_expr + <||> PQuery . Not <$$ keyword "!?" <**> value_expr + <||> keyword "?-" **> opt_foreach PInstQuery <||> PDeclBlock <$$> declarations diff --git a/src/Language/EFLINT/Print.hs b/src/Language/EFLINT/Print.hs --- a/src/Language/EFLINT/Print.hs +++ b/src/Language/EFLINT/Print.hs @@ -16,6 +16,9 @@ ppPhrase :: Phrase -> String ppPhrase p = case p of PQuery t -> "?" ++ ppTerm t + PInstQuery vs t + | null vs -> "?-" ++ ppTerm t + | otherwise -> "?-" ++ foreach vs (ppTerm t) PDo t -> ppTagged t PTrigger vs t -> foreach vs $ ppTerm t Create vs t -> "+" ++ foreach vs (ppTerm t) @@ -37,6 +40,9 @@ CTerminate vs t -> "-" ++ foreach vs (ppTerm t) CObfuscate vs t -> "~" ++ foreach vs (ppTerm t) CQuery t -> "?" ++ ppTerm t + CInstQuery vs t + |null vs -> "?-" ++ ppTerm t + |otherwise -> "?-" ++ foreach vs (ppTerm t) CPDir dir -> case dir of DirInv ty -> "Invariant " ++ ty @@ -81,11 +87,12 @@ ] -- TODO print syncs(?) +-- TODO recipient? ppAct' domainID domain domain_constr clauses = - "Act " ++ domainID ++ " Actor " ++ ppVar actor ++ " Recipient " ++ ppVar recipient ++ show_objects + "Act " ++ domainID ++ " Actor " ++ ppVar actor ++ show_objects ++ ppConstraint (domain_constr) ++ ppClauses clauses - where Products (actor:recipient:objects) = domain + where Products (actor:objects) = domain show_objects | null objects = "" | otherwise = " Related to " ++ intercalate ", " (map (\(Var x dec) -> x++dec) objects) diff --git a/src/Language/EFLINT/Spec.hs b/src/Language/EFLINT/Spec.hs --- a/src/Language/EFLINT/Spec.hs +++ b/src/Language/EFLINT/Spec.hs @@ -7,6 +7,8 @@ import qualified Data.Map as M import qualified Data.Set as S +import Control.Monad (join) + import Data.Aeson hiding (String) import qualified Data.Aeson as JSON @@ -53,10 +55,14 @@ data Kind = Fact FactSpec | Act ActSpec | Duty DutySpec | Event EventSpec deriving (Ord, Eq, Show, Read) +data Restriction = VarRestriction | FunctionRestriction + deriving (Ord, Eq, Show, Read, Enum) + data TypeSpec = TypeSpec { kind :: Kind , domain :: Domain , domain_constraint :: Term + , restriction :: Maybe Restriction , derivation :: [Derivation] , closed :: Bool {- whether closed world assumption is made for this type -} , conditions :: [Term] @@ -73,14 +79,17 @@ deriving (Ord, Eq, Show, Read) data DutySpec = DutySpec { - enforcing_acts :: [DomId] --TODO consider moving to outer ast - , violated_when :: [Term] + enforcing_acts :: [DomId] -- for record-keeping only, semantics in static-eval + , terminating_acts :: [DomId] -- for record-keeping only, semantics in static-eval + , creating_acts :: [DomId] -- for record-keeping only, semantics in static-eval + , violated_when :: [Term] } deriving (Ord, Eq, Show, Read) data ActSpec = ActSpec { effects :: [Effect] - , syncs :: [Sync] + , syncs :: [Sync] + , physical :: Bool } deriving (Ord, Eq, Show, Read) @@ -93,7 +102,8 @@ deriving (Ord, Eq, Show, Read) data EventSpec = EventSpec { - event_effects :: [Effect] + event_effects :: [Effect] + , event_syncs :: [Sync] } deriving (Ord, Eq, Show, Read) @@ -124,6 +134,7 @@ emptySpec = Spec { decls = built_in_decls, aliases = M.empty} where built_in_decls = M.fromList [ ("int", int_decl) + , ("string", string_decl) , (actor_ref_address, string_decl) -- used for actor identifiers , ("actor", actor_decl) ] @@ -137,6 +148,16 @@ where op d tspec res | null (derivation tspec) = res | otherwise = S.insert d res +is_var :: Spec -> DomId -> Bool +is_var spec d = case join $ fmap restriction (M.lookup d (decls spec)) of + Just VarRestriction -> True + _ -> False + +is_function :: Spec -> DomId -> Bool +is_function spec d = case join $ fmap restriction (M.lookup d (decls spec)) of + Just FunctionRestriction -> True + _ -> False + -- type-environment pairs, restricting either: -- * the components of the initial state (all instantiations of restricted by ) -- (can be thought of as the Genesis transition, constructing the Garden of Eden) @@ -164,6 +185,7 @@ | Terminate [Var] Term | Obfuscate [Var] Term | PQuery Term + | PInstQuery [Var] Term | PDeclBlock [Decl] | PSkip deriving (Eq, Show, Read) @@ -173,11 +195,16 @@ | PlaceholderDecl DomId DomId deriving (Eq, Show, Read) -introducesName :: Decl -> Bool -introducesName (TypeDecl _ _) = True -introducesName (TypeExt _ _) = False -introducesName (PlaceholderDecl _ _) = True +data CDecl = CTypeDecl DomId TypeSpec + | CTypeExt DomId [CModClause] + | CPlaceholderDecl DomId DomId + deriving (Eq, Show, Read) +isInitialTypeDecl :: Decl -> Bool +isInitialTypeDecl (TypeDecl _ _) = True +isInitialTypeDecl (TypeExt _ _) = False +isInitialTypeDecl (PlaceholderDecl _ _) = False + extend_spec :: [Decl] -> Spec -> Spec extend_spec = flip (foldr op) where op (TypeDecl ty tyspec) spec = spec { decls = M.insert ty tyspec (decls spec) } @@ -190,31 +217,57 @@ | SyncCl [Sync] | ViolationCl [Term] | EnforcingActsCl [DomId] + | TerminatedByCl [DomId] + | CreatedByCl [DomId] deriving (Eq, Show, Read) -apply_ext :: DomId -> [ModClause] -> Spec -> Spec -apply_ext ty clauses spec = case find_decl spec ty of - Nothing -> spec - Just tspec -> spec { decls = M.insert ty (apply_type_ext ty clauses tspec) (decls spec) } - -apply_type_ext :: DomId -> [ModClause] -> TypeSpec -> TypeSpec +data CModClause = CConditionedByCl [Term] + | CDerivationCl [Derivation] + | CPostCondCl [Effect] + | CSyncCl [Sync] + | CViolationCl [Term] + | CEnforcingActsCl [DomId] + | CTerminatedByCl [DomId] + | CCreatedByCl [DomId] + deriving (Eq, Show, Read) + +enforcing_act_condition :: DomId {- act id -}-> Term +enforcing_act_condition a = Enabled (App a (Right [])) + +terminated_by_condition :: DomId {- duty id -} -> DomId {- act id -} -> Term +terminated_by_condition d a = App d (Right []) + +terminated_by_precondition :: DomId {- duty id -} -> DomId {- act id -} -> Term +terminated_by_precondition d a = Present (App d (Right [])) + +created_by_condition :: DomId {- duty id -} -> DomId {- act id -} -> Term +created_by_condition d a = App d (Right []) + +apply_type_ext :: DomId -> [CModClause] -> TypeSpec -> TypeSpec apply_type_ext ty clauses tspec = foldr apply_clause tspec clauses where apply_clause clause tspec = case clause of - ConditionedByCl conds -> tspec { conditions = conds ++ conditions tspec } - DerivationCl dvs -> tspec { derivation = dvs ++ derivation tspec } - PostCondCl effs -> tspec { kind = add_effects (kind tspec) } + CConditionedByCl conds -> tspec { conditions = conds ++ conditions tspec } + CDerivationCl dvs -> tspec { derivation = dvs ++ derivation tspec } + CPostCondCl effs -> tspec { kind = add_effects (kind tspec) } where add_effects (Act aspec) = Act (aspec { effects = effs ++ effects aspec}) add_effects (Event espec)= Event (espec { event_effects = effs ++ event_effects espec }) add_effects s = s - SyncCl ss -> tspec { kind = add_syncs (kind tspec) } + CSyncCl ss -> tspec { kind = add_syncs (kind tspec) } where add_syncs (Act aspec) = Act $ aspec { syncs = ss ++ syncs aspec} + add_syncs (Event espec) = Event $ espec { event_syncs = ss ++ event_syncs espec} add_syncs s = s - ViolationCl vs -> tspec { kind = add_viol_conds (kind tspec) } + CViolationCl vs -> tspec { kind = add_viol_conds (kind tspec) } where add_viol_conds (Duty dspec) = Duty $ dspec { violated_when = vs ++ violated_when dspec } add_viol_conds s = s - EnforcingActsCl ds -> tspec { kind = add_enf_acts (kind tspec) } + CEnforcingActsCl ds -> tspec { kind = add_enf_acts (kind tspec) } where add_enf_acts (Duty dspec) = Duty $ dspec { enforcing_acts = ds ++ enforcing_acts dspec } add_enf_acts s = s + CTerminatedByCl as -> tspec { kind = add_terms_acts (kind tspec) } + where add_terms_acts (Duty dspec) = Duty $ dspec { terminating_acts = as ++ terminating_acts dspec } + add_terms_acts s = s + CCreatedByCl as -> tspec { kind = add_create_acts (kind tspec) } + where add_create_acts (Duty dspec) = Duty $ dspec { creating_acts = as ++ creating_acts dspec } + add_create_acts s = s data CPhrase = CDo Tagged -- execute computed instance | CTrigger [Var] Term -- execute instance to be computed @@ -222,6 +275,7 @@ | CTerminate [Var] Term | CObfuscate [Var] Term | CQuery Term + | CInstQuery [Var] Term | CPOnlyDecls | CPDir CDirective | CSeq CPhrase CPhrase @@ -466,6 +520,7 @@ actor_decl = TypeSpec { kind = Fact (FactSpec False True) , domain = AnyString , domain_constraint = BoolLit True + , restriction = Nothing , derivation = [] , conditions = [] , closed = True @@ -475,6 +530,7 @@ int_decl = TypeSpec { kind = Fact (FactSpec False False) , domain = AnyInt , domain_constraint = BoolLit True + , restriction = Nothing , derivation = [] , closed = True , conditions = [] } @@ -486,6 +542,7 @@ string_decl = TypeSpec { kind = Fact (FactSpec False False) , domain = AnyString , domain_constraint = BoolLit True + , restriction = Nothing , derivation = [] , closed = True , conditions = [] } @@ -495,6 +552,7 @@ TypeSpec { kind = Fact (FactSpec False False) , domain = Strings ss , domain_constraint = BoolLit True + , restriction = Nothing , derivation = [] , closed = True , conditions = [] } diff --git a/src/Language/EFLINT/State.hs b/src/Language/EFLINT/State.hs --- a/src/Language/EFLINT/State.hs +++ b/src/Language/EFLINT/State.hs @@ -50,37 +50,43 @@ store_unions :: [Store] -> Store store_unions = foldr store_union emptyStore -make_assignments :: Store -> State -> State -make_assignments = flip (M.foldrWithKey op) - where op te HoldsTrue = create te +make_assignments :: Spec -> Store -> State -> State +make_assignments spec = flip (M.foldrWithKey op) + where op te@(_,d) HoldsTrue | is_var spec d = var_assignment te + | is_function spec d = function_assignment te + | otherwise = create te op te HoldsFalse = terminate te op te Unknown = obfuscate te -derive :: Tagged -> State -> State -derive te s = s { contents = M.alter adj te (contents s) } - where adj Nothing = Just $ Info{ value = True, from_sat = True } - adj (Just info) = Just info + create :: Tagged -> State -> State + create te s = s { contents = M.insert te Info{ value = True, from_sat = False } (contents s) } -derive_all :: [Tagged] -> State -> State -derive_all = flip (foldr derive) + terminate :: Tagged -> State -> State + terminate te s = s { contents = M.insert te Info{ value = False, from_sat = False } (contents s) } -create :: Tagged -> State -> State -create te s = s { contents = M.insert te Info{ value = True, from_sat = False } (contents s) } + obfuscate :: Tagged -> State -> State + obfuscate te s = s { contents = M.delete te (contents s) } -create_all :: [Tagged] -> State -> State -create_all = flip (foldr create) + var_assignment :: Tagged -> State -> State + var_assignment te@(_,d) s = create te $ s { contents = M.mapWithKey op (contents s) } + where op te@(_,d') i | d == d' = i { value = False, from_sat = False } + | otherwise = i -terminate :: Tagged -> State -> State -terminate te s = s { contents = M.insert te Info{ value = False, from_sat = False } (contents s) } + function_assignment :: Tagged -> State -> State + function_assignment te@(Product [f,t], d) s = + create te $ s { contents = M.mapWithKey op (contents s) } + where op (Product [f',t'], d') i | d == d' && f == f' = i { value = False, from_sat = False } + op _ i = i + function_assignment _ s = s -terminate_all :: [Tagged] -> State -> State -terminate_all = flip (foldr terminate) -obfuscate :: Tagged -> State -> State -obfuscate te s = s { contents = M.delete te (contents s) } +derive :: Tagged -> State -> State +derive te s = s { contents = M.alter adj te (contents s) } + where adj Nothing = Just $ Info{ value = True, from_sat = True } + adj (Just info) = Just info -obfuscate_all :: [Tagged] -> State -> State -obfuscate_all = flip (foldr obfuscate) +derive_all :: [Tagged] -> State -> State +derive_all = flip (foldr derive) -- | assumes the instance of a closed type holds :: Tagged -> State -> Bool diff --git a/src/Language/EFLINT/StaticEval.hs b/src/Language/EFLINT/StaticEval.hs --- a/src/Language/EFLINT/StaticEval.hs +++ b/src/Language/EFLINT/StaticEval.hs @@ -9,7 +9,7 @@ import Control.Applicative import Data.Maybe (isNothing) -import Data.List ((\\)) +import Data.List ((\\), partition) import qualified Data.Map as M import qualified Data.Set as S @@ -47,12 +47,15 @@ get_spec :: M_Stc Spec get_spec = M_Stc $ \spec -> Right (spec, spec) -execute_decl :: Decl -> M_Stc () +insert_typespec :: DomId -> TypeSpec -> M_Stc () +insert_typespec ty tspec = M_Stc $ \spec -> Right (spec { decls = M.insert ty tspec (decls spec) }, ()) + +execute_decl :: CDecl -> M_Stc () execute_decl decl = M_Stc $ \spec -> let spec' = case decl of - PlaceholderDecl f t -> spec { aliases = M.insert f t (aliases spec) } - TypeExt ty clauses -> spec { decls = M.adjust (apply_type_ext ty clauses) ty (decls spec) } - TypeDecl ty tspec -> spec { decls = M.insert ty tspec (decls spec) } + CPlaceholderDecl f t -> spec { aliases = M.insert f t (aliases spec) } + CTypeExt ty clauses -> spec { decls = M.adjust (apply_type_ext ty clauses) ty (decls spec) } + CTypeDecl ty tspec -> spec { decls = M.insert ty tspec (decls spec) } in Right (spec', ()) with_spec :: Spec -> M_Stc a -> M_Stc a @@ -117,9 +120,18 @@ Terminate vs t -> fmap (de_stmt p) (compile_stmt (to_stmt p)) Obfuscate vs t -> fmap (de_stmt p) (compile_stmt (to_stmt p)) PQuery t -> fmap (de_stmt p) (compile_stmt (to_stmt p)) + PInstQuery vs t -> do + fs <- free_vars t + let unbounds = S.toList (fs `S.difference` S.fromList vs) + CInstQuery (vs ++ unbounds) . fst <$> compile_term t PDeclBlock ds -> do - forM_ (filter introducesName ds) execute_decl - forM_ ds ((execute_decl =<<) . compile_decl) + -- introduce new types first + let (type_decls, others) = partition isInitialTypeDecl ds + forM_ type_decls (\(TypeDecl d tspec) -> insert_typespec d tspec) + -- then process other type declarations + forM_ others $ \decl -> do + decls <- compile_decl decl + forM_ decls execute_decl return CPOnlyDecls where to_stmt (PTrigger vs t) = Trans vs Trigger (Left t) to_stmt (Create vs t) = Trans vs AddEvent (Left t) @@ -134,28 +146,40 @@ de_stmt (PQuery t) (Query t') = CQuery t' de_stmt _ _ = error "Explorer.assert 2" -compile_decl :: Decl -> M_Stc Decl -compile_decl d@(PlaceholderDecl x y) = check_known_type [no_decoration y] >> return d +compile_decl :: Decl -> M_Stc [CDecl] +compile_decl d@(PlaceholderDecl x y) = check_known_type [no_decoration y] + >> return [CPlaceholderDecl x y] compile_decl d@(TypeExt ty clauses) = compile_ext ty clauses -compile_decl d@(TypeDecl ty tspec) = compile_type_spec ty tspec +compile_decl d@(TypeDecl ty tspec) = (:[]) <$> compile_type_spec ty tspec -compile_ext :: DomId -> [ModClause] -> M_Stc Decl +compile_ext :: DomId -> [ModClause] -> M_Stc [CDecl] compile_ext ty clauses = do spec <- get_spec case M.lookup ty (decls spec) of Nothing -> err ("cannot find the type " ++ ty ++ " to extend or " ++ ty ++ " of the wrong kind") - Just tspec -> TypeExt ty <$> mapM (compile_clause ty tspec) clauses + Just tspec -> concat <$> mapM (compile_clause ty tspec) clauses where compile_clause ty tspec clause = case clause of - ConditionedByCl conds -> ConditionedByCl <$> mapM (convert_precon ty tspec) conds - DerivationCl dvs -> DerivationCl <$> mapM (compile_derivation xs ty) dvs - PostCondCl effs -> PostCondCl <$> mapM (compile_effect xs) effs - SyncCl ss -> SyncCl <$> mapM (compile_sync xs) ss - ViolationCl vts -> ViolationCl <$> mapM (compile_violation_condition ty) vts - EnforcingActsCl ds -> return $ EnforcingActsCl ds + ConditionedByCl conds -> to_ext ty . CConditionedByCl <$> mapM (convert_precon ty tspec) conds + DerivationCl dvs -> to_ext ty . CDerivationCl <$> mapM (compile_derivation xs ty) dvs + PostCondCl effs -> to_ext ty . CPostCondCl <$> mapM (compile_effect xs) effs + SyncCl ss -> to_ext ty . CSyncCl <$> mapM (compile_sync xs) ss + ViolationCl vts -> to_ext ty . CViolationCl <$> mapM (compile_violation_condition ty) vts + EnforcingActsCl as -> do viols <- mapM compile_enf as + return $ CTypeExt ty [CEnforcingActsCl as] : viols + where compile_enf a = CTypeExt ty . (:[]) . CViolationCl . (:[]) . fst <$> compile_term (enforcing_act_condition a) + TerminatedByCl as -> do posts <- mapM compile_termby as + holds <- mapM compile_holdsby as + return $ [CTypeExt ty [CTerminatedByCl as]] ++ posts ++ holds + where compile_termby a = CTypeExt a . (:[]) . CPostCondCl . (:[]) <$> compile_effect' TAll xs [] (terminated_by_condition ty a) + compile_holdsby a = CTypeExt a . (:[]) . CDerivationCl . (:[]) <$> compile_derivation xs a (HoldsWhen (terminated_by_precondition ty a)) + CreatedByCl as -> do posts <- mapM compile_createdby as + return $ [CTypeExt ty [CCreatedByCl as]] ++ posts + where compile_createdby a = CTypeExt a . (:[]) . CPostCondCl . (:[]) <$> compile_effect' CAll xs [] (created_by_condition ty a) where xs = case domain tspec of Products xs -> xs _ -> [no_decoration ty] + to_ext ty clause = [CTypeExt ty [clause]] -compile_type_spec :: DomId -> TypeSpec -> M_Stc Decl +compile_type_spec :: DomId -> TypeSpec -> M_Stc CDecl compile_type_spec ty tspec = do with_decl ty tspec $ do -- ensure the declaration is active during its compilation dom <- get_dom ty @@ -171,7 +195,8 @@ let domain_constraint = case S.toList (ffs `S.difference` S.fromList xs) of [] -> dom_filter vars -> Exists vars dom_filter - return (TypeDecl ty (TypeSpec {domain = domain tspec, closed = closed tspec,..})) + return (CTypeDecl ty (TypeSpec {domain = domain tspec, closed = closed tspec + ,restriction = restriction tspec, ..})) check_domain :: DomId -> Domain -> M_Stc () check_domain dty (Products xs) = check_known_type xs @@ -207,18 +232,14 @@ Event espec -> do let Products xs = domain tspec effects' <- sequence (map (compile_effect xs) (event_effects espec)) - return (Event (espec { event_effects = effects' } )) - Duty dspec -> do -- TODO, should be dealt with by outer -> inner translation - e_conds <- concat <$> mapM select_condition (enforcing_acts dspec) - vconds <- mapM (compile_violation_condition ty) (e_conds ++ violated_when dspec) - return $ (Duty (dspec { violated_when = vconds })) - where select_condition a = do - spec <- get_spec - case M.lookup a (decls spec) of - Just tspec | Act _ <- kind tspec -> return [foldr And (BoolLit True) (conditions tspec)] - _ -> err ("duty " ++ ty ++ " is declared with enforcing act " ++ a ++ " which is not a declared or not declared as an act") + -- convert syncs + syncs' <- mapM (compile_sync xs) (event_syncs espec) + return (Event (espec { event_effects = effects', event_syncs = syncs' } )) + Duty dspec -> do vconds <- mapM (compile_violation_condition ty) (violated_when dspec) + return $ (Duty (dspec { violated_when = vconds })) Fact _ -> return k + compile_violation_condition :: DomId -> Term -> M_Stc Term compile_violation_condition dty term = do domain <- get_dom dty @@ -244,8 +265,8 @@ spec <- get_spec ds <- sequence (map (uncurry compile_type_spec) (M.toList (decls spec))) let tspecs = concatMap op ds - where op (TypeDecl ty tspec) = [(ty,tspec)] - op _ = [] + where op (CTypeDecl ty tspec) = [(ty,tspec)] + op _ = [] return (spec {decls = decls_union (decls spec) (M.fromList tspecs) }) compile_derivation :: [Var] -> DomId -> Derivation -> M_Stc Derivation @@ -302,13 +323,16 @@ compile_effect :: [Var] -> Effect -> M_Stc Effect compile_effect bound eff = case eff of - TAll xs t -> compile_effect' TAll xs t - CAll xs t -> compile_effect' CAll xs t - OAll xs t -> compile_effect' OAll xs t - where compile_effect' cons xs t = do (t',tau) <- compile_term t - fs <- free_vars t' - let unbounds = S.toList (fs `S.difference` S.fromList (bound ++ xs)) - return (cons (xs ++ unbounds) t') + TAll xs t -> compile_effect' TAll bound xs t + CAll xs t -> compile_effect' CAll bound xs t + OAll xs t -> compile_effect' OAll bound xs t + +compile_effect' :: ([Var] -> Term -> Effect) -> [Var] -> [Var] -> Term -> M_Stc Effect +compile_effect' cons bound xs t = do + (t',tau) <- compile_term t + fs <- free_vars t' + let unbounds = S.toList (fs `S.difference` S.fromList (bound ++ xs)) + return (cons (xs ++ unbounds) t') compile_term :: Term -> M_Stc (Term, Type) compile_term t0 = do diff --git a/src/REPL.hs b/src/REPL.hs --- a/src/REPL.hs +++ b/src/REPL.hs @@ -81,8 +81,8 @@ let state = make_initial_state spec i' let explorer = init_explorer (Just (spec,state)) let ((_,c0),_,(sid, ctx)) = get_last_edge explorer (EI.currRef explorer) - verbosity opts 1 $ display_commands - verbosity opts 2 $ display_info opts [] c0 ctx + verbosity opts Default $ display_commands + verbosity opts Default $ display_info opts [] c0 ctx runInputT defaultSettings (repl opts explorer) Left errs -> putStrLn "compilation errors:" >> putStrLn (unlines errs) @@ -102,14 +102,9 @@ Nothing -> return () Just input -> do case span (not . isSpace) input of - (":choose", mint) -> repl_trigger ctx mint - (":revert", mint) | Just sid' <- readMaybe (dropWhile isSpace mint) - -> case run_ exp (Revert sid') of - InvalidRevert -> outputStrLn ("state id " ++ show sid' ++ " unknown") >> continue exp - ResultTrans exp outs (old,_) (new,sid) -> do - lift (display_info opts outs old new) - continue exp - | otherwise -> lift display_commands >> continue exp + (":choose", mint) -> repl_trigger ctx mint + (":jump", mint) -> revert_or_jump False mint sid + (":revert", mint) -> revert_or_jump True mint sid (":display", _) -> lift (display ctx) >> continue exp (":d", _) -> lift (display ctx) >> continue exp (":spec", mty) -> lift (display_spec ctx mty) >> continue exp @@ -139,6 +134,13 @@ Left err -> outputStrLn err >> continue exp Right ps -> repl_phrases opts emptyInput ps exp >>= continue + revert_or_jump destr mint sid = case readMaybe (dropWhile isSpace mint) of + Just sid' -> case run_ exp (Revert sid' destr) of + InvalidRevert -> outputStrLn ("state id " ++ show sid' ++ " unknown") >> continue exp + ResultTrans exp outs (old,_) (new,sid) -> + lift (display_info opts outs old new) >> continue exp + _ -> lift display_commands >> continue exp + repl_directive_phrases :: Options -> [Either Directive Phrase] -> Explorer -> InputT IO Explorer repl_directive_phrases opts [] explorer = return explorer repl_directive_phrases opts (edp:ps) explorer = @@ -190,7 +192,7 @@ Response -> Explorer -> InputT IO Explorer repl_report opts inpm phrases res exp = case res of ResultTrans exp outs (old,_) (ctx,sid) -> case missing_inputs outs of - [] -> lift (verbosity opts 3 (display_info opts outs old ctx)) >> return exp + [] -> lift (verbosity opts TestMode (display_info opts outs old ctx)) >> return exp ms -> do minpm <- foldM consider (Just inpm) ms case minpm of Just inpm' -> repl_phrases opts inpm' phrases exp Nothing -> return exp @@ -224,17 +226,21 @@ display_info :: Options -> [Output] -> Config -> Config -> IO () display_info opts outs c0 cfg = do - verbosity opts 4 $ display_errors (errors outs) - verbosity opts 5 $ display_query_results (query_ress outs) - verbosity opts 6 $ display_transitions (ex_triggers outs) - verbosity opts 7 $ display_violations (violations outs) - verbosity opts 8 $ display_new_types (M.keysSet $ decls $ cfg_spec c0) (M.keysSet $ decls $ cfg_spec cfg) - verbosity opts 9 $ display_fact_changes (cfg_state c0) (cfg_state cfg) - verbosity opts 10$ display_new_invariants (invariants $ cfg_spec c0) (invariants $ cfg_spec cfg) + verbosity opts TestMode $ display_errors (errors outs) + verbosity opts TestMode $ display_query_results (query_ress outs) + verbosity opts TestMode $ display_inst_query_results (inst_query_ress outs) + verbosity opts Default $ display_transitions (ex_triggers outs) + verbosity opts Default $ display_violations (violations outs) + verbosity opts Default $ display_new_types (M.keysSet $ decls $ cfg_spec c0) (M.keysSet $ decls $ cfg_spec cfg) + verbosity opts Default $ display_fact_changes (cfg_state c0) (cfg_state cfg) + verbosity opts Default $ display_new_invariants (invariants $ cfg_spec c0) (invariants $ cfg_spec cfg) where display_query_results [] = return () display_query_results ress = mapM_ op ress - where op QuerySuccess = verbosity opts 11 (putStrLn "query successful") - op QueryFailure = verbosity opts 12 (putStrLn "query failed") + where op QuerySuccess = verbosity opts Default (putStrLn "query successful") + op QueryFailure = verbosity opts TestMode (putStrLn "query failed") + + display_inst_query_results vss = forM_ vss $ \vs -> do mapM_ (putStrLn . ppTagged) vs + putStrLn "" display_errors [] = return () display_errors errs = mapM_ op errs diff --git a/src/Server.hs b/src/Server.hs --- a/src/Server.hs +++ b/src/Server.hs @@ -175,6 +175,7 @@ let outs = S.fromList (ex_triggers outputs) let errs = S.fromList (errors outputs) let qress = query_ress outputs + let iqress = inst_query_ress outputs let transitions = S.fromList (rest_transitions ctx) let new_duties = S.fromList (rest_duties ctx) S.\\ S.fromList (rest_duties c0) @@ -185,7 +186,7 @@ let response = case missing_inputs outputs of [] -> CommandSuccess old_id state_id facts_from facts_to created_facts terminated_facts - viols outs errs qress + viols outs errs qress iqress new_duties all_duties new_enabled new_disabled transitions ms -> InputRequired ms @@ -200,7 +201,7 @@ CreateEvent term inpm -> compile_and inpm $ Program (Create [] term) TerminateEvent term inpm -> compile_and inpm $ Program (Terminate [] term) QueryCommand term inpm -> compile_and inpm $ Program (PQuery term) - Revert new_state -> report $ run_ exp (Explorer.Revert new_state) + Revert new_state destr -> report $ run_ exp (Explorer.Revert new_state destr) Status mid -> report $ run_ exp (Display (maybe (EI.currRef exp) id mid)) History mid -> report $ run_ exp (DisplayFull (maybe (EI.currRef exp) id mid)) Heads -> report $ run_ exp ExplorationHeads @@ -239,7 +240,7 @@ | CreateEvent Term InputMap | TerminateEvent Term InputMap | QueryCommand Term InputMap - | Revert Int + | Revert Int Bool {- whether the revert is destructive or not -} | Status (Maybe Int) | Kill | GetFacts InputMap @@ -261,7 +262,7 @@ "test-absent" -> QueryCommand . Not . value_to_term <$> v .: "value" <*> maybe_input v "enabled" -> QueryCommand . Enabled . value_to_term <$> v .: "value" <*> maybe_input v - "revert" -> Revert <$> v .: "value" + "revert" -> Revert <$> v .: "value" <*> (v .: "destructive" <|> return False) "action" -> full_action <|> trigger_action where full_action = actionCommand <$> @@ -364,7 +365,8 @@ (S.Set Violation) (S.Set TransInfo) (S.Set Error) -- errors: compilation + transition - [QueryRes] -- query results + [QueryRes] -- query results + [[Tagged]] -- instance query results (S.Set Tagged) -- new duties (S.Set Tagged) -- all duties in the current state (S.Set Tagged) -- newly enabled transitions @@ -384,7 +386,7 @@ toJSON (InvalidCommand err) = object [ "response" .= JSON.String "invalid command", "message" .= toJSON err ] toJSON (CommandSuccess sid_from i facts_from facts_to created_facts terminated_facts - vs outs errs qress + vs outs errs qress iqress new_duties all_duties new_enabled new_disabled all_transitions) = object [ "response" .= JSON.String "success" @@ -399,6 +401,7 @@ , "output-events" .= toJSON outs , "errors" .= toJSON errs , "query-results" .= toJSON qress + , "inst-query-results" .= toJSON (map TaggedJSON (concat iqress)) , "new-duties" .= toJSON (map TaggedJSON $ S.toList new_duties) , "new-enabled-transitions" .= toJSON (map TaggedJSON $ S.toList new_enabled) @@ -541,6 +544,7 @@ toJSON (ExecutedTransition info) = object [ "output-type" .= JSON.String "executed-transition", "info" .= toJSON info] toJSON (Violation v) = object [ "output-type" .= JSON.String "violation", "output" .= v] toJSON (QueryRes r) = object [ "output-type" .= JSON.String "query-res", "output" .= r] + toJSON (InstQueryRes vs)= object [ "output-type" .= JSON.String "inst-query-res", "output" .= toJSON (map TaggedJSON vs)] toJSON (ErrorVal e) = object [ "output-type" .= JSON.String "error-val", "output" .= e] instance FromJSON Output where @@ -637,9 +641,14 @@ kind <- o .: "kind" domain <- o .: "domain" domain_constraint <- o .: "domain_constraint" + restriction_text <- (Just <$> o .: "restriction" <|> return Nothing) derivation <- o .: "derivation" closed <- o .: "closed" conditions <- o .: "conditions" + let restriction = case restriction_text::Maybe String of + Just "var" -> Just VarRestriction + Just "function" -> Just FunctionRestriction + _ -> Nothing return TypeSpec{..} instance ToJSON Kind where @@ -677,13 +686,15 @@ instance ToJSON ActSpec where toJSON actspec = object [ "effects" .= effects actspec, - "syncs" .= syncs actspec + "syncs" .= syncs actspec, + "physical" .= physical actspec ] instance FromJSON ActSpec where parseJSON = withObject "actspec" $ \o -> do effects <- o .: "effects" syncs <- o .: "syncs" + physical <- o .: "physical" return ActSpec{..} instance ToJSON Term where @@ -870,24 +881,30 @@ instance ToJSON DutySpec where toJSON dutyspec = object [ - "enforcing_acts" .= enforcing_acts dutyspec, - "violated_when" .= violated_when dutyspec + "enforcing_acts" .= enforcing_acts dutyspec, + "violated_when" .= violated_when dutyspec, + "terminating_acts" .= terminating_acts dutyspec, + "creating_acts" .= creating_acts dutyspec ] instance FromJSON DutySpec where parseJSON = withObject "dutyspec" $ \o -> do enforcing_acts <- o.: "enforcing_acts" + terminating_acts <- o.: "terminating_acts" + creating_acts <- o.: "creating_acts" violated_when <- o.: "violated_when" return DutySpec{..} instance ToJSON EventSpec where toJSON eventspec = object [ - "event_effects" .= event_effects eventspec + "event_effects" .= event_effects eventspec + , "event_syncs" .= event_syncs eventspec ] instance FromJSON EventSpec where parseJSON = withObject "eventspec" $ \o -> do event_effects <- o.: "event_effects" + event_syncs <- o.: "event_syncs" return EventSpec{..} instance ToJSON Domain where