diff --git a/eflint.cabal b/eflint.cabal --- a/eflint.cabal +++ b/eflint.cabal @@ -1,28 +1,28 @@ -cabal-version: >=1.10 +cabal-version: 2.0 name: eflint -version: 3.1.0.2 -synopsis: Simulation interpreter for FLINT policy descriptions +version: 4.1.0.1 +synopsis: Reference interpreter for eFLINT specifications and scenario evaluation description: Software systems that share potentially sensitive data are subjected to laws, regulations, policies and/or contracts. The monitoring, control and enforcement processes applied to these systems are currently to a large extent manual, which we rather automate by embedding the processes as dedicated and adaptable software services in order to improve efficiency and effectiveness. This approach requires such regulatory services to be closely aligned with a formal description of the relevant norms. . eFLINT is a domain-specific language developed for formalizing norms from a variety of sources. The theoretical foundations of the language are found in transition systems and in Hohfeld’s framework of legal fundamental conceptions. The language can be used to formalize norms from a large variety of sources. The resulting specifications are executable and support several forms of reasoning such as automatic case assessment, manual exploration and simulation. Moreover, the specifications can be used to develop regulatory services for several types of monitoring, control and enforcement. The language is evaluated through a case study formalizing articles 6(1)(a) and 16 of the General Data Protection Regulation (GDPR). . - Related papers: - . - *eFLINT: a Domain-Specific Language for Executable Norm Specifications. Proceedings of GPCE '20. L. Thomas van Binsbergen, Lu-Chi Liu, Robert van Doesburg, and Tom van Engers. . - *Dynamic generation of access control policies from social policies. Proceedings of The 11th International Conference on Current and Future Trends of Information and Communication Technologies in Healthcare (ICTH 2021). Procedia Computer Science 198C (2022) pp. 140-147. L. Thomas van Binsbergen, Milen G. Kebede, Joshua Baugh, Tom van Engers, Dannis G. van Vuurden. + The main academic paper is to be cited as follows. + . + *Reflections on the design, applications and implementations of eFLINT, a domain-specific language for legal compliance reasoning. L. Thomas van Binsbergen, Christopher A. Esterhuyse, Tim Müller. Journal of Computer Languages. Volume 88, 2026. . . - Preprints available at + More related papers and preprints available at bug-reports: https://gitlab.com/eflint/haskell-implementation -homepage: http://cci-research.nl +homepage: https://gitlab.com/eflint license: BSD3 license-file: LICENSE author: L. Thomas van Binsbergen maintainer: ltvanbinsbergen@acm.org -copyright: Copyright (C) 2019-2022 L. Thomas van Binsbergen +copyright: Copyright (C) 2019-2020 Centrum Wiskunde & Informatica (CWI), + Copyright (C) 2019- University of Amsterdam (UvA) category: Language build-type: Simple extra-source-files: CHANGELOG.md @@ -34,6 +34,7 @@ Language.EFLINT.Parse Language.EFLINT.Print Language.EFLINT.StaticEval + Language.EFLINT.FormExtraction Language.EFLINT.Eval Language.EFLINT.Saturation Language.EFLINT.Binders @@ -44,22 +45,19 @@ Language.EFLINT.Options build-depends: base >=4.9 && < 5 , containers >=0.5 && <0.7 - , hxt >= 9.3.1.16 - , time >= 1.8.0.2 - , gll >= 0.4.1.0 - , regex-applicative >= 0.3.3 - , aeson >= 1.4.6.0 - , bytestring >= 0.10.8.2 - , network >= 3.1 - , text >= 1.2.4.0 - , filepath >= 1.4.2 - , directory >= 1.3.6 - , exploring-interpreters >= 1.4.0.0 - , fgl >= 5.7 - , mtl >= 2.2 + , gll ^>= 0.4.1 + , regex-applicative ^>= 0.3.3 + , aeson ^>= 2.3 + , bytestring ^>= 0.11 + , network ^>= 3.1 + , text ^>= 1.2.4 + , filepath ^>= 1.4.2 + , directory ^>= 1.3.6 + , exploring-interpreters ^>= 1.4.0 + , mtl ^>= 2.2 hs-source-dirs: src default-language: Haskell2010 - ghc-options: -fwarn-incomplete-patterns -fwarn-unused-imports + ghc-options: -fwarn-incomplete-patterns -fwarn-unused-imports -fwarn-unused-packages executable eflint-repl main-is: REPL.hs @@ -78,23 +76,18 @@ Language.EFLINT.Options build-depends: base >=4.9 && < 5 , containers >=0.5 && <0.7 - , hxt >= 9.3.1.16 - , time >= 1.8.0.2 - , 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 - , mtl >= 2.2 - , haskeline >= 0.8.1 - , transformers >= 0.5.6 - , exploring-interpreters >= 1.4.0.0 - , text + , gll ^>= 0.4.1 + , regex-applicative ^>= 0.3.3 + , aeson ^>= 2.3 + , filepath ^>= 1.4.2 + , directory ^>= 1.3.6 + , mtl ^>= 2.2 + , haskeline ^>= 0.8.1 + , transformers ^>= 0.5.6 + , exploring-interpreters ^>= 1.4.0 hs-source-dirs: src default-language: Haskell2010 - ghc-options: -fwarn-incomplete-patterns -fwarn-unused-imports + ghc-options: -fwarn-incomplete-patterns -fwarn-unused-imports -fwarn-unused-packages library exposed-modules : Language.EFLINT.State @@ -113,18 +106,13 @@ Language.EFLINT.Options build-depends: base >=4.9 && < 5 , containers >=0.5 && <0.7 - , hxt >= 9.3.1.16 - , time >= 1.8.0.2 - , 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.4.0.0 - , fgl >= 5.7 - , mtl >= 2.2 + , gll ^>= 0.4.1 + , regex-applicative ^>= 0.3.3 + , aeson ^>= 2.3 + , filepath ^>= 1.4.2 + , directory ^>= 1.3.6 + , exploring-interpreters ^>= 1.4.0 + , mtl ^>= 2.2 hs-source-dirs: src default-language: Haskell2010 - ghc-options: -fwarn-incomplete-patterns -fwarn-unused-imports + ghc-options: -fwarn-incomplete-patterns -fwarn-unused-imports -fwarn-unused-packages 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 @@ -8,30 +8,28 @@ import Control.Monad import Control.Applicative -import Data.Bool (bool) -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] } +data M_Subs a = M_Subs { runSubs :: Spec -> State -> Subs -> Either RuntimeError [a] } err :: RuntimeError -> M_Subs a -err re = M_Subs $ \spec state inpm subs -> Left re +err re = M_Subs $ \spec state subs -> Left re nd :: [a] -> M_Subs a -nd vals = M_Subs $ \spec state inpm subs -> return vals +nd vals = M_Subs $ \spec state subs -> return vals results :: M_Subs a -> M_Subs [a] -results n = M_Subs $ \spec state inpm subs -> (:[]) <$> runSubs n spec state inpm subs +results n = M_Subs $ \spec state subs -> (:[]) <$> runSubs n spec state subs ignoreMissingInput :: M_Subs a -> M_Subs a -ignoreMissingInput m = M_Subs $ \spec state inpm subs -> case runSubs m spec state inpm subs of +ignoreMissingInput m = M_Subs $ \spec state subs -> case runSubs m spec state subs of Left (MissingInput _) -> Right [] res -> res bind :: Var -> Tagged -> M_Subs a -> M_Subs a -bind k v m = M_Subs $ \spec state inpm -> runSubs m spec state inpm . M.insert k v +bind k v m = M_Subs $ \spec state -> runSubs m spec state . M.insert k v scope_var :: Var -> M_Subs a -> M_Subs a scope_var x m = do @@ -39,44 +37,36 @@ bind x te m get_type_spec :: DomId -> M_Subs TypeSpec -get_type_spec d = M_Subs $ \spec state inpm subs -> +get_type_spec d = M_Subs $ \spec state subs -> case find_decl spec d of Nothing -> Left (InternalError (UndeclaredType d)) Just tspec -> Right [tspec] get_dom :: DomId -> M_Subs (Domain, Term) -get_dom d = M_Subs $ \spec state inpm subs -> +get_dom d = M_Subs $ \spec state subs -> case find_decl spec d of Nothing -> Left (InternalError (UndeclaredType d)) Just tspec -> Right [(domain tspec, domain_constraint tspec)] get_time :: M_Subs Int -get_time = M_Subs $ \spec state inpm subs -> return [time state] +get_time = M_Subs $ \spec state subs -> return [time state] get_subs :: M_Subs Subs -get_subs = M_Subs $ \spec state inpm subs -> return [subs] +get_subs = M_Subs $ \spec state subs -> return [subs] modify_subs :: (Subs -> Subs) -> M_Subs a -> M_Subs a -modify_subs mod m = M_Subs $ \spec state inpm -> runSubs m spec state inpm . mod +modify_subs mod m = M_Subs $ \spec state -> runSubs m spec state . mod get_spec :: M_Subs Spec -get_spec = M_Subs $ \spec state inpm subs -> return [spec] +get_spec = M_Subs $ \spec state subs -> return [spec] get_state :: M_Subs State -get_state = M_Subs $ \spec state inpm subs -> return [state] - -get_input :: M_Subs InputMap -get_input = M_Subs $ \spec state inpm subs -> return [inpm] - -get_input_assignment :: Tagged -> M_Subs Assignment -get_input_assignment te = M_Subs $ \spec state inpm subs -> - Right [maybe Unknown (bool HoldsFalse HoldsTrue) (M.lookup te inpm)] +get_state = M_Subs $ \spec state subs -> return [state] get_assignment :: Tagged -> M_Subs Assignment -get_assignment te@(_,d) = M_Subs $ \spec state inpm subs -> +get_assignment te@(_,d) = M_Subs $ \spec state subs -> Right [maybe Unknown op (M.lookup te (contents state))] - where op info | from_sat info = Unknown - | value info = HoldsTrue + where op info | value info = HoldsTrue | otherwise = HoldsFalse instance Functor M_Subs where @@ -87,17 +77,17 @@ (<*>) = ap instance Monad M_Subs where - return a = M_Subs $ \spec state inpm subs -> return [a] - (>>=) m f = M_Subs $ \spec state inpm subs -> do - as <- runSubs m spec state inpm subs - let op res a = (++res) <$> runSubs (f a) spec state inpm subs + return a = M_Subs $ \spec state subs -> return [a] + (>>=) m f = M_Subs $ \spec state subs -> do + as <- runSubs m spec state subs + let op res a = (++res) <$> runSubs (f a) spec state subs foldM op [] as instance Alternative M_Subs where - empty = M_Subs $ \spec state inpm subs -> return [] - m1 <|> m2 = M_Subs $ \spec state inpm subs -> do - xs <- runSubs m1 spec state inpm subs - ys <- runSubs m2 spec state inpm subs + empty = M_Subs $ \spec state subs -> return [] + m1 <|> m2 = M_Subs $ \spec state subs -> do + xs <- runSubs m1 spec state subs + ys <- runSubs m2 spec state subs return (xs ++ ys) instance MonadPlus M_Subs where @@ -122,49 +112,62 @@ every_valid_subs :: Var -> M_Subs Tagged every_valid_subs x = do spec <- get_spec + state <- get_state let d = remove_decoration spec x (dom, _) <- get_dom d - if enumerable spec dom then generate_instances d - else every_available_subs spec d - where generate_instances d = do + let (trues,falses) = assigned_instances state d + let gen_assigned = trues ++ falses + let gen_holds = trues + let generate_instances = do (dom, dom_filter) <- get_dom d e <- instantiate_domain d dom let bindings = case (dom,e) of (Products xs, Product args) -> M.fromList (zip xs args) _ -> M.singleton (no_decoration d) (e,d) modify_subs (`subsUnion` bindings) (checkTrue (eval dom_filter)) return (e,d) - every_available_subs spec d = do - state <- get_state - inpm <- get_input - nd [ te | te@(v,d') <- state_input_holds state inpm, d' == d ] + let every_available_subs spec = + case closed_type spec d of + Just False | null gen_assigned -> -- open type and no assignments made in K.B. + err (MissingInput (MissingInstances d (flatten_domain spec dom) (restriction_of spec d))) + | otherwise -> nd $ gen_holds + _ -> nd gen_holds + if enumerable spec dom + then generate_instances + else every_available_subs spec --- if fact/duty/event/action is of an inenumerable type, is derived with "Holds when" and is not in state, --- then check if it is a valid instance and whether it satisfies derivation clause --- if so, consider it to hold true -is_in_virtual_state :: Tagged -> M_Subs Bool -is_in_virtual_state te@(_,d) = do +flatten_domain :: Spec -> Domain -> MDomain +flatten_domain spec dom = case dom of + AnyString -> MAnyString + AnyInt -> MAnyInt + Time -> MAnyInt -- deprecated + Ints is -> MInts is + Strings ss -> MStrings ss + Products vs -> MProducts (map elem_from_var vs) + where elem_from_var var = (d, flatten_domain spec dom) + where d = remove_decoration spec var + dom = domain (decls spec M.! d) + + +is_holds :: Tagged -> M_Subs Bool +is_holds te@(_,d) = do + state <- get_state spec <- get_spec is_valid_instance te >>= \case False -> return False True -> do - get_input_assignment te >>= \case - HoldsTrue -> return True - HoldsFalse -> return False - Unknown -> do get_assignment te >>= \case HoldsTrue -> return True HoldsFalse -> return False - Unknown -> do - is_derivable te >>= \case - True -> return True - False -> case fromJust (closed_type spec d) of + Unknown -> + case fromJust (closed_type spec d) of True -> return False - False -> err (MissingInput te) + False -> let (trues, falses) = assigned_instances state d + in err (MissingInput $ missing_assignments trues falses [te] (restriction_of spec d)) is_enabled :: Tagged -> M_Subs Bool is_enabled v@(e,d) = do spec <- get_spec - is_in_virtual_state v >>= \case + is_holds v >>= \case False -> return False True -> sat_conditions v >>= \case False -> return False @@ -194,29 +197,6 @@ True -> check_constraint _ -> return False -is_derivable :: Tagged -> M_Subs Bool -is_derivable te@(e,d) = derivation_closure_on te $ do - spec <- get_spec - (dom, _) <- get_dom d - let bindings = case (dom,e) of (Products xs, Product args) -> M.fromList (zip xs args) - _ -> M.singleton (no_decoration d) te - let consider_clause deriv = case deriv of - Dv xs dvt -> do tes <- modify_subs (`subsUnion` bindings) - (foreach (xs \\ M.keys bindings) (whenTagged (eval dvt) return)) - return (te `elem` tes) -- valid instance and in DV - HoldsWhen t -> modify_subs (`subsUnion` bindings) (whenBool (eval t) return ) - case fmap derivation (find_decl spec d) of - Nothing -> return False - Just dvs -> (or <$> mapM consider_clause dvs) >>= \case - True -> sat_conditions te - False -> return False - -derivation_closure_on :: Tagged -> M_Subs Bool -> M_Subs Bool -derivation_closure_on te m = M_Subs $ \spec state inpm subs -> case M.lookup te (contents state) of - Just info -> return [value info] - Nothing -> runSubs m spec (mod state) inpm subs - where mod s = s { contents = M.insert te (Info { value = False, from_sat = True }) (contents s) } - sat_conditions :: Tagged -> M_Subs Bool sat_conditions te@(v,d) = is_valid_instance te >>= \case @@ -229,7 +209,7 @@ modify_subs (`subsUnion` bindings) (and <$> mapM (flip whenBool return . eval) (conditions tspec)) is_violated :: Tagged -> M_Subs Bool -is_violated te@(_,d) = (&&) <$> is_in_virtual_state te <*> violation_condition te +is_violated te@(_,d) = (&&) <$> is_holds te <*> violation_condition te where violation_condition te = do spec <- get_spec eval_violation_condition te (find_violation_cond spec d) @@ -245,7 +225,7 @@ syncTransInfos :: [TransInfo] -> (Store, Bool {- forced? -}) syncTransInfos = foldr op (emptyStore, False) - where op (TransInfo te ass is_f is_a tes) (ass',is_f') = + where op (TransInfo te ass is_f is_d is_a tes) (ass',is_f') = (ass `store_union` ass', is_f || is_f') instantiate_trans :: Tagged -> M_Subs TransInfo @@ -260,10 +240,10 @@ 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) (event_syncs espec) + Act aspec -> do_transition te actor is_enabled (effects aspec) (syncs aspec) (physical aspec) + Event espec -> do_transition te Nothing is_enabled (event_effects espec) (event_syncs espec) True where done = te `S.insert` done' - do_transition te@(v,d) mActor is_enabled effects ss = do + do_transition te@(v,d) mActor is_enabled effects ss is_physical = do (dom, _) <- get_dom d let Products xs = dom let Product args = v @@ -272,7 +252,9 @@ let (ss_ass,any_f) = syncTransInfos sync_infos ass' <- store_unions <$> mapM eval_effect effects let ass = ass' `store_union` ss_ass - return (TransInfo te ass (any_f || not is_enabled) mActor sync_infos) + let disabled = any_f || not is_enabled -- assumes any synch'ed trans is institutional + let forced = any_f || (not is_enabled && not is_physical) + return (TransInfo te ass forced disabled mActor sync_infos) actor = case v of Product (a:objs) -> Just a _ -> Nothing @@ -288,7 +270,7 @@ eval_effect (OAll xs t) = M.fromList . map (,Unknown) <$> foreach xs (whenTagged (eval t) return) get_kind :: DomId -> M_Subs Kind -get_kind d = M_Subs $ \spec state inpm subs -> return $ maybe [] (:[]) (find_kind spec d) +get_kind d = M_Subs $ \spec state subs -> return $ maybe [] (:[]) (find_kind spec d) where find_kind :: Spec -> DomId -> Maybe Kind find_kind spec d = fmap kind (find_decl spec d) @@ -304,6 +286,12 @@ checkFalse m = m >>= \case ResBool False -> return () _ -> empty +checkFilter :: (a -> M_Subs Bool) -> M_Subs a -> M_Subs a +checkFilter p m = do + a <- m + b <- p a + case b of True -> return a + False -> empty whenInt :: M_Subs Value -> (Int -> M_Subs a) -> M_Subs a whenInt m f = m >>= \case ResInt v -> f v @@ -316,7 +304,7 @@ whenTagged m f = m >>= \case ResTagged v -> f v _ -> empty -whenTaggedHolds m f = m >>= \case ResTagged v -> is_in_virtual_state v >>= \case +whenTaggedHolds m f = m >>= \case ResTagged v -> is_holds v >>= \case True -> f v False -> empty _ -> empty @@ -334,7 +322,8 @@ Ref x -> ResTagged <$> substitute_var x App d params-> do (dom,dom_filter) <- get_dom d case dom of - Products xs -> do + Products xs -> do -- this code relies on StaticEval to ensure any parameters not mentioned as + -- arguments are bound under the name of the parameter, see use of `xs` below let replacements = make_substitutions_of xs params tes <- mapM (\(x,t) -> whenTagged (eval t) (return . (x,))) replacements args <- modify_subs (`subsUnion` M.fromList tes) (mapM substitute_var xs) @@ -376,7 +365,7 @@ False -> empty) {- whenBool (eval t2) $ \case True -> eval t1 False -> empty-} - Present t1 -> whenTagged (eval t1) (\v -> ResBool <$> is_in_virtual_state v) + Present t1 -> whenTagged (eval t1) (\v -> ResBool <$> is_holds v) Violated t1 -> whenTagged (eval t1) (\v -> ResBool <$> is_violated v) Enabled t1 -> whenTagged (eval t1) (\v -> ResBool <$> is_enabled v) Exists xs t -> ResBool . not . null <$> results (foldr scope_var (checkTrue (eval t)) xs) 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 @@ -3,7 +3,7 @@ module Language.EFLINT.Explorer where import Language.EFLINT.Spec (Spec, Phrase(PSkip), ppTagged) -import Language.EFLINT.State (State, emptyInput, InputMap, TransInfo(..), Assignment(..), trans_is_action) +import Language.EFLINT.State (State, TransInfo(..), Assignment(..), trans_is_action) import Language.EFLINT.Interpreter (Program(..), Config(..), interpreter, initialConfig, Output, getOutput) import Language.EFLINT.Print() @@ -14,10 +14,10 @@ type Explorer = EI.Explorer Label Config [Output] -type Label = (InputMap, Program) +type Label = Program -data Instruction = Execute [Program] InputMap - | ExecuteOnce Program InputMap +data Instruction = Execute [Program] + | ExecuteOnce Program | 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 @@ -71,7 +71,7 @@ HoldsFalse -> "-" ++ ppTagged te Unknown -> "~" ++ ppTagged te whether_enabled | not (trans_is_action info) = "" - | trans_forced info = "(DISABLED)" + | trans_disabled info = "(DISABLED)" | otherwise = "(ENABLED)" triggerTree :: TransInfo -> Tree TransInfo @@ -80,7 +80,7 @@ get_last_edge :: Explorer -> Ref -> ((Ref, Config), (Label, [Output]), (Ref, Config)) get_last_edge exp cr = case reverse (EI.getPathFromTo exp 1 cr) of (edge:_) -> edge - _ -> maybe (error ("ASSERT: get_last_edge1")) (\cfg -> ((cr,cfg), ((emptyInput, Program PSkip),[]), (cr,cfg))) (EI.deref exp cr) + _ -> maybe (error ("ASSERT: get_last_edge1")) (\cfg -> ((cr,cfg), ((Program PSkip),[]), (cr,cfg))) (EI.deref exp cr) init_tree_explorer, init_graph_explorer :: Maybe (Spec,State) -> Explorer init_tree_explorer = EI.mkExplorer False (const . const $ False) defInterpreter . initialConfig @@ -90,13 +90,13 @@ run_ :: Explorer -> Instruction -> Response run_ exp instr = case instr of - Execute ps inpm -> - let (exp',outs) = EI.executeAll (map (inpm,) ps) exp + Execute ps -> + let (exp',outs) = EI.executeAll ps exp cfg' = EI.config exp' ref' = EI.currRef exp' in ResultTrans exp' outs (EI.config exp, EI.currRef exp) (cfg', ref') - ExecuteOnce ps inpm -> - let (exp',outs) = EI.execute (inpm,ps) exp + ExecuteOnce ps -> + let (exp',outs) = EI.execute ps exp cfg' = EI.config exp' ref' = EI.currRef exp' in ResultTrans exp' outs (EI.config exp, EI.currRef exp) (cfg', ref') diff --git a/src/Language/EFLINT/FormExtraction.hs b/src/Language/EFLINT/FormExtraction.hs new file mode 100644 --- /dev/null +++ b/src/Language/EFLINT/FormExtraction.hs @@ -0,0 +1,54 @@ +{-# LANGUAGE TupleSections #-} + +module Language.EFLINT.FormExtraction where + +import Language.EFLINT.Spec +import Language.EFLINT.State +import Language.EFLINT.Eval + +import Data.List ((\\)) +import qualified Data.Map as M +import qualified Data.Set as S + +form_all_open :: Spec -> State -> S.Set MissingInput +form_all_open spec = form_from_set (M.keysSet (decls spec)) spec + +form_from_phrases :: [Phrase] -> Spec -> State -> S.Set MissingInput +form_from_phrases ps spec state = form_from_set reachables spec state + where reachables = S.unions (map (reachable spec) ps) + +reachable :: Spec -> Phrase -> S.Set DomId +reachable spec p = M.keysSet (decls spec) +{- + PDo Tagged + | PTrigger [Var] Term + | Create [Var] Term + | Terminate [Var] Term + | Obfuscate [Var] Term + | PQuery Term + | PInstQuery [Var] Term + | PDeclBlock [Decl] + | PSkip + -} + +reachable_term :: Spec -> Term -> S.Set DomId +reachable_term spec term = S.empty + +reachable_foreach :: Spec -> [Var] -> Term -> S.Set DomId +reachable_foreach spec vars t = + S.fromList (map (remove_decoration spec) vars) `S.union` reachable_term spec t + +form_from_set :: S.Set DomId -> Spec -> State -> S.Set MissingInput +form_from_set set spec state = + S.map (mk_missing spec state) $ S.filter isOpen set + where isOpen d = case closed_type spec d of Just False -> True + _ -> False + +mk_missing :: Spec -> State -> DomId {- open -} -> MissingInput +mk_missing spec state d = + case runSubs (every_valid_subs (no_decoration d)) spec state M.empty of + Left (MissingInput mi) -> mi -- either MissingAssignments or MissingInstances + Left err -> error $ "assert 2 mk_missing" ++ print_runtime_error err + Right tes -> missing_assignments trues falses ((tes \\ trues) \\ falses) (restriction_of spec d) + where (trues, falses) = assigned_instances state d + 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 @@ -3,6 +3,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, inst_query_ress, missing_inputs + ,missing_assignments, missing_instances_for ,convert_programs, collapse_programs) where import Language.EFLINT.Eval @@ -26,7 +27,7 @@ data Config = Config { cfg_spec :: Spec , cfg_state :: State - , rest_transitions :: [Transition] -- (label * enabled?) -- replaced + , rest_transitions :: [Transition] -- (label * violating?) -- replaced , rest_duties :: [Tagged] -- replaced after ever step } deriving (Eq) @@ -45,14 +46,15 @@ collapse_programs [] = ProgramSkip collapse_programs programs = (foldr1 PSeq programs) -interpreter :: (InputMap, Program) -> Config -> OutputWriter (Maybe Config) -interpreter (inpm, Program p) cfg = case runStatic (compile_phrase p) (ctx_spec ctx) of +interpreter :: Program -> Config -> OutputWriter (Maybe Config) +interpreter (Program p) cfg = case runStatic (compile_phrase p) (ctx_spec ctx) of Left err -> tell [ErrorVal (CompilationError (unlines err))] >> return Nothing - Right (spec', p') -> fmap context2config <$> sem_phrase p' inpm - (ctx{ctx_spec = spec', ctx_state = rebase_and_sat spec' (ctx_state ctx)}) + Right (spec', p') -> sem_phrase p' (ctx{ctx_spec = spec'}) >>= \case + Nothing -> return Nothing + Just sto -> fmap context2config <$> new_context spec' (ctx_state ctx) sto where ctx = config2context cfg -interpreter (inpm, PSeq p1 p2) cfg = (interpreter (inpm,p1) cfg) >>= interpreter (inpm,p2) . maybe cfg id -interpreter (inpm, ProgramSkip) cfg = return Nothing +interpreter (PSeq p1 p2) cfg = (interpreter p1 cfg) >>= interpreter p2 . maybe cfg id +interpreter (ProgramSkip) cfg = return Nothing initialConfig Nothing = context2config (emptyContext emptySpec) initialConfig (Just (spec,state)) = context2config $ @@ -105,74 +107,92 @@ where op (InstQueryRes vs) = [vs] op _ = [] -missing_inputs :: [Output] -> [Tagged] +missing_inputs :: [Output] -> [MissingInput] missing_inputs = S.toList . S.fromList . concatMap op - where op (ErrorVal (RuntimeError (MissingInput te))) = [te] + where op (ErrorVal (RuntimeError (MissingInput miss))) = [miss] op _ = [] +missing_instances_for :: [MissingInput] -> [(DomId, MDomain, Maybe Restriction)] +missing_instances_for = concatMap op + where op (MissingAssignments tes _) = [] + op (MissingInstances d dom mres) = [(d,dom,mres)] + type OutputWriter = Writer [Output] getOutput :: OutputWriter a -> (a,[Output]) getOutput = runWriter -error_or_process :: M_Subs a -> Spec -> State -> InputMap -> ([a] -> OutputWriter (Maybe Context)) -> OutputWriter (Maybe Context) -error_or_process ma spec state inpm fa = case runSubs ma spec state inpm emptySubs of +do_saturation :: Spec -> State -> OutputWriter (Maybe State) +do_saturation spec state = case runSubs (rebase_and_sat spec state) spec state emptySubs of + Right [state'] -> return (Just state') + Right _ -> error "assert do_saturation: no or ambiguous saturation result" + Left err -> tell [ErrorVal $ RuntimeError err] >> return Nothing + +error_or_process :: M_Subs a -> Spec -> State -> ([a] -> OutputWriter (Maybe b)) -> OutputWriter (Maybe b) +error_or_process ma spec state fa = case runSubs ma spec state emptySubs of Left err -> tell [ErrorVal $ RuntimeError err] >> return Nothing Right as -> fa as -sem_phrase :: CPhrase -> InputMap -> Context -> OutputWriter (Maybe Context) -sem_phrase p inpm c0 = case p of +new_context :: Spec -> State -> Store -> OutputWriter (Maybe Context) +new_context spec state ass = do_saturation spec (make_assignments spec ass state) >>= \case + Nothing -> return Nothing + Just state' -> do + let duties = [ te | te@(v,d) <- (state_holds state') + , Duty _ <- maybe [] (:[]) (fmap kind (find_decl spec d)) ] + error_or_process (find_duty_violations duties) spec state' $ \d_viols -> + error_or_process (find_inv_violations (S.toList $ invariants spec)) spec state' $ \i_viols -> do + tell (map Violation (concat d_viols ++ concat i_viols)) + error_or_process find_transitions spec state' $ \tss -> + return $ Just $ Context + { ctx_state = state' + , ctx_spec = spec + , ctx_transitions = concat tss + , ctx_duties = duties + } + + +sem_phrase :: CPhrase -> Context -> OutputWriter (Maybe Store) +sem_phrase p c0 = case p of CPSkip -> return Nothing CPOnlyDecls -> no_effect - CQuery t -> error_or_process (eval t) spec state inpm $ \vs -> do + CQuery t -> error_or_process (eval t) spec state $ \vs -> do let queryRes | all (== (ResBool True)) vs = QuerySuccess | otherwise = QueryFailure tell [QueryRes queryRes] >> no_effect CInstQuery b vs t -> let t' | b = When t (Present t) | otherwise = t - in error_or_process (foreach vs (whenTagged (eval t') return)) spec state inpm $ \vs -> + in error_or_process (foreach vs (whenTagged (eval t') return)) spec state $ \vs -> 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) - CDo te -> error_or_process (trigger_or_fail te) spec state inpm consider_transinfos + CDo te -> error_or_process (trigger_or_fail te) spec state consider_transinfos CTrigger vs t -> let m_subs = do tes <- foreach vs (whenTagged (eval t) return) case tes of (te@(_,d):_) | triggerable spec d -> Right <$> forM tes instantiate_trans | otherwise -> return (Left d) _ -> return (Right []) - in error_or_process m_subs spec state inpm consider_transinfos - CPDir dir -> return_context emptyStore [dir] - CSeq p q -> sem_phrase p inpm c0 >>= (sem_phrase q inpm . maybe c0 id) + in error_or_process m_subs spec state consider_transinfos + CPPar p1 p2 -> do mc1 <- sem_phrase p1 c0 + mc2 <- sem_phrase p2 c0 + case (mc1, mc2) of + (Just c1, Just c2) -> return (Just $ c1 `store_union` c2) + _ -> return Nothing +-- (Just c1, Nothing) -> return mc1 +-- (Nothing, Just c2) -> return mc2 +-- (Nothing, Nothing) -> return Nothing where spec = ctx_spec c0 state = ctx_state c0 - return_context :: Store -> [CDirective] -> OutputWriter (Maybe Context) - return_context ass dirs = do - let duties = [ te | te@(v,d) <- (state_input_holds state' inpm) - , Duty _ <- maybe [] (:[]) (fmap kind (find_decl spec' d)) ] - error_or_process (find_duty_violations duties) spec' state' inpm $ \d_viols -> - error_or_process (find_inv_violations (S.toList $ invariants spec')) spec' state' inpm $ \i_viols -> do - tell (map Violation (concat d_viols ++ concat i_viols)) - error_or_process find_transitions spec' state' inpm $ \tss -> - return $ Just $ c0 - { ctx_state = state' - , ctx_spec = spec' - , ctx_transitions = concat tss - , ctx_duties = duties - } - where state' = rebase_and_sat spec (make_assignments spec' ass state) - spec' = process_directives dirs spec - - no_effect :: OutputWriter (Maybe Context) - no_effect = return_context emptyStore [] + no_effect :: OutputWriter (Maybe Store) + no_effect = return $ Just emptyStore - single_effect :: Effect -> OutputWriter (Maybe Context) + single_effect :: Effect -> OutputWriter (Maybe Store) single_effect eff = - error_or_process (eval_effect eff) spec state inpm $ \stores -> - return_context (M.unions stores) {- always just one store-} [] + error_or_process (eval_effect eff) spec state $ \stores -> + return (Just $ M.unions stores) {- always just one store-} trigger_or_fail :: Tagged -> M_Subs (Either DomId [TransInfo]) trigger_or_fail te@(_,d) | triggerable spec d = Right . (:[]) <$> instantiate_trans te @@ -182,7 +202,7 @@ consider_transinfos [Right infos] = do forM_ infos $ \info -> do tell [ExecutedTransition info] tell_violations info - return_context (store_unions (map trans_assignments infos)) [] + return (Just $ store_unions (map trans_assignments infos)) consider_transinfos _ = error "ASSERT: consider_transinfos" tell_violations :: TransInfo -> OutputWriter () @@ -217,7 +237,7 @@ concat <$> mapM gen_trans (trigger_decls spec) where gen_trans (d,_) = results $ ignoreMissingInput $ do tagged <- every_possible_subs (no_decoration d) - exist <- is_in_virtual_state tagged + exist <- is_enabled tagged return Transition{..} every_possible_subs :: Var -> M_Subs Tagged @@ -243,14 +263,16 @@ return (Product args, d) _ -> do state <- get_state - input <- get_input - nd $ [ te | te@(v,d') <- state_input_holds state input, d' == d ] + nd $ [ te | te@(v,d') <- state_holds state, d' == d ] make_initial_state :: Spec -> Initialiser -> State -make_initial_state spec inits = do - case runSubs (store_unions <$> mapM eval_effect inits) spec emptyState emptyInput emptySubs of +make_initial_state spec inits = + let make_inits = do + sto <- store_unions <$> mapM eval_effect inits + rebase_and_sat spec (make_assignments spec sto emptyState) + in case runSubs make_inits spec emptyState emptySubs of Left err -> error (print_runtime_error err) Right res -> case res of - [] -> error "failed to initialise state" - [sto] -> rebase_and_sat spec (make_assignments spec sto emptyState) - _ -> error "non-deterministic state initialisation" + [] -> error "failed to initialise state" + [state] -> state + _ -> 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 @@ -32,7 +32,7 @@ , domain_constraint = BoolLit True , restriction = Nothing , derivation = [HoldsWhen condition_term] - , closed = True + , closed = Nothing , conditions = [] } where condition_term = foldr And (BoolLit True) $ @@ -41,8 +41,8 @@ , Ref (no_decoration (interested_party a))] ++ (map Ref objects) 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) + aspec = ActSpec { effects = map mkT (act_terminate a) + ++ map mkC (act_create a) , syncs = [] , physical = False } where mkT ob = case ob of ImplicitDV expr -> tAll [] expr @@ -62,10 +62,10 @@ ,no_decoration (claimant d)] ++ objects , domain_constraint = BoolLit True , restriction = Nothing - , derivation = case (derivation :: Duty -> Maybe Binder) d of + , derivation = case duty_derivation d of Nothing -> [] Just b -> [dv (duty d) (vars b) (binder_expression b)] - , closed = True + , closed = Nothing , conditions = [] } where dspec = DutySpec {enforcing_acts = maybe [] (:[]) (enforcing d) @@ -78,7 +78,7 @@ tFact :: Fact -> (DomId, TypeSpec) tFact f = (fact f,) $ TypeSpec { kind = Spec.Fact fspec - , domain = case (domain :: Fact -> Maybe Language.EFLINT.JSON.Domain) f of + , domain = case fact_domain f of Nothing -> case function f of ImplicitDV (RefExpr (BaseVar "[]")) -> AnyString _ -> Products [] @@ -91,7 +91,7 @@ RefExpr (BaseVar "<<>>") -> [] expr -> [dv (fact f) [] expr] ExplicitDV d -> [dv (fact f) (vars d) (binder_expression d)] - , closed = False + , closed = Nothing , conditions = [] } where fspec = FactSpec { invariant = False, Spec.actor = False } @@ -182,9 +182,9 @@ , object :: String , interested_party :: String , preconditions :: Expression - , create :: [OptBinder] - , terminate :: [OptBinder] - , derivation :: Maybe Binder + , act_create :: [OptBinder] + , act_terminate :: [OptBinder] + , act_derivation :: Maybe Binder , sources :: Maybe [Source] , explanation :: Maybe String , version :: Maybe String @@ -201,7 +201,7 @@ data Fact = Fact { fact :: String , function :: OptBinder - , domain :: Maybe Language.EFLINT.JSON.Domain + , fact_domain :: Maybe Language.EFLINT.JSON.Domain , sources :: Maybe [Source] , explanation :: Maybe String , version :: Maybe String @@ -232,10 +232,8 @@ , duty_components :: String , duty_holder :: String , claimant :: String - , create :: String - , terminate :: String , enforcing :: Maybe String - , derivation :: Maybe Binder + , duty_derivation :: Maybe Binder , sources :: Maybe [Source] , explanation :: Maybe String , version :: Maybe String 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 @@ -16,10 +16,11 @@ lexer_settings :: LexerSettings lexer_settings = emptyLanguage { identifiers = types + , signed_int_lits = False , 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", "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" + , "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", "Domain" , "Do", "Placeholder", "For", "Not", "Open", "Closed", "?-", "?--" , "#", "##", "###", "####" , "#include", "#require" @@ -161,7 +162,6 @@ <||> (:[]) <$$> placeholder where fact = syn_fact_decl (make_fact False False) <||> 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 :: Bool -> Bool -> Bool -> Maybe Restriction -> DomId -> Domain -> Term -> [ModClause] -> [Decl] @@ -172,7 +172,7 @@ , domain_constraint = dom_filter , restriction = restr , derivation = [] - , closed = is_closed + , closed = if is_closed then Nothing else Just False , conditions = [] } 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 @@ -188,7 +188,7 @@ domain_constraint = dom_filter, restriction = Nothing, derivation = [], - closed = is_closed, + closed = if is_closed then Nothing else Just False, conditions = [] } actor = maybe (no_decoration "actor") id mact @@ -201,7 +201,7 @@ domain_constraint = dom_filter, restriction = Nothing, derivation = [], - closed = True, + closed = Nothing, conditions = [] } actor = maybe (no_decoration "actor") id mact holds_true = DerivationCl [HoldsWhen (BoolLit True)] @@ -215,7 +215,7 @@ , domain_constraint = dom_filter , restriction = Nothing , derivation = [] - , closed = is_closed + , closed = if is_closed then Nothing else Just False , conditions = [] } @@ -229,14 +229,14 @@ kind = Duty (DutySpec { violated_when = [], enforcing_acts = [] , terminating_acts = [], creating_acts = [] }), derivation = [], - closed = is_closed, + closed = if is_closed then Nothing else Just False, conditions = []} 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 <**> fact_restriction_by_keyword <**> id_lit <**> optionalWithDef (keyword "Identified by" **> type_expr) AnyString <**> - syn_domain_constraint <**> + syn_domain_constraint <**>>> -- prefers initial Identified by clause over extension (the two are ambiguous if only one Identified by clause is given). NOTE, example of ambiguity where in one case (Strings) the two interpretations are equivalent and in the other cases (Ints) type-checking could resolve the ambiguity syn_fact_clauses fact_restriction_by_keyword :: BNF Token (Maybe Restriction) @@ -264,14 +264,6 @@ syn_fact_ext :: BNF Token Decl syn_fact_ext = "fact-type-ext" <:=> TypeExt <$$ keyword "Fact" <**> id_lit <**> syn_fact_clauses -syn_actor_decl :: (Bool -> DomId -> Domain -> Term -> [ModClause] -> a) -> BNF Token a -syn_actor_decl cons = "actor-type-decl" <:=> cons' <$$> - syn_is_closed <** keyword "Actor" <**> id_lit <**> - optionalWithDef (keyword "With" **> manySepBy1 var (keychar '*')) [] <**> - syn_domain_constraint <**> - syn_fact_clauses - where cons' isc d vars t = cons isc d (Products (Var actor_ref_address "" : vars)) t - syn_pred_decl :: (DomId -> Term -> a) -> BNF Token a syn_pred_decl cons = "pred-type-decl" <:=> cons <$$ keyword "Predicate" <**> id_lit <** keyword_when <**> value_expr @@ -308,8 +300,6 @@ 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 @@ -326,10 +316,13 @@ syn_fact_clauses = multiple syn_fact_clause where syn_fact_clause = "fact-clause" <:=> ConditionedByCl <$$> precondition' <||> DerivationCl <$$> derivation_from + <||> open_or_close + <||> extend_domain_clauses syn_physical_clauses :: BNF Token [ModClause] syn_physical_clauses = multiple syn_physical_clause where syn_physical_clause = "physical-clause" <:=> ConditionedByCl <$$> precondition' + <||> open_or_close <||> PostCondCl <$$> creating_post' <||> PostCondCl <$$> terminating_post' <||> PostCondCl <$$> obfuscating_post' @@ -339,6 +332,7 @@ syn_event_clauses = multiple syn_event_clause where syn_event_clause = "event-clause" <:=> ConditionedByCl <$$> precondition' <||> DerivationCl <$$> derivation_from + <||> open_or_close <||> PostCondCl <$$> creating_post' <||> PostCondCl <$$> terminating_post' <||> PostCondCl <$$> obfuscating_post' @@ -348,6 +342,7 @@ syn_duty_clauses = multiple syn_duty_clause where syn_duty_clause = "duty-clause" <:=> ConditionedByCl <$$> precondition' <||> DerivationCl <$$> derivation_from + <||> open_or_close <||> ViolationCl <$$> violation_condition <||> EnforcingActsCl <$$> enforcing_acts_clauses <||> TerminatedByCl <$$> terminated_by_clauses @@ -433,6 +428,22 @@ <||> "Holds when" <$$ keyword "Present when" <||> keyword "Holds when" +extend_domain_clauses :: BNF Token ModClause +extend_domain_clauses = "extend-domain-clauses" + <:=> (keyword "Identified by" <||> keyword "Domain") **> + (StringsCl <$$> manySepBy1 atom (keychar '+' <||> keychar ',') + <||> IntsCl <$$> manySepBy1 int_lit (keychar '+' <||> keychar ',') + <||> ints_from_domain <$$> int_lit <** keyword ".." <**> int_lit + <||> strings_from_domain <$$> char_lit <** keyword ".." <**> char_lit) + where ints_from_domain min max = IntsCl $ [min..max] + strings_from_domain min max = StringsCl $ map (:[]) [min..max] + + +open_or_close :: BNF Token ModClause +open_or_close = "open-or-closed-clause" + <:=> Close <$$ keyword "Closed" + <||> Open <$$ keyword "Open" + -- parsing refiner specifications parse_refiner :: String -> Either String Refiner parse_refiner = parse_component refiner @@ -474,18 +485,31 @@ phrase_scenario = "phrase-scenario" <:=> multiple (syn_phrase <** keychar '.') syn_directives_phrases :: BNF Token [Either Directive Phrase] -syn_directives_phrases = "opt.directives.phrases" <:=> optionalWithDef - (someSepBy1 (Left <$$> syn_directive <||> Right <$$> syn_phrase) (keychar '.') - <** optional (keychar '.')) [] +syn_directives_phrases = "opt.directives.phrases" <:=> top_level_unite <$$> optionalWithDef + (many1 (Left <$$> syn_directive <** keychar '.' + <||> Right <$$> syn_phrase_or_comp)) [] + <**> (fmap Right <$$> optional syn_phrase) -- optional phrase *without* full stop +top_level_unite :: [a] -> Maybe a -> [a] +top_level_unite ps mp = maybe ps ((ps++) . (:[])) mp + syn_directive :: BNF Token Directive syn_directive = "directive" <:=> Include <$$ keyword "#include" <**> string_lit <||> Require <$$ keyword "#require" <**> string_lit syn_phrases :: BNF Token [Phrase] -syn_phrases = "opt.phrase" <:=> optionalWithDef - (someSepBy1 syn_phrase (keychar '.') <** optional (keychar '.')) [] +syn_phrases = syn_top_level + +syn_top_level :: BNF Token [Phrase] +syn_top_level = "top-level-phrases" <:=> top_level_unite <$$> + optionalWithDef (many1 syn_phrase_or_comp) [] <**> + optional syn_phrase -- optional phrase *without* full stop + +syn_phrase_or_comp = "parallel-comp" <:=> + PParBlock <$$> braces ( optionalWithDef + (manySepBy1 syn_phrase (keychar '.') <** optional (keychar '.')) [] + ) <||> syn_phrase <** keychar '.' syn_phrase :: BNF Token Phrase syn_phrase = "phrase" 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 @@ -28,27 +28,24 @@ Obfuscate vs t -> "~" ++ foreach vs (ppTerm t) PSkip -> "" PDeclBlock ds -> unlines (map ppDecl ds) + PParBlock ps -> unlines $ intersperse ";" $ map ppPhrase ps ppCPhrase :: CPhrase -> String ppCPhrase p = case p of CPSkip -> "" CPOnlyDecls -> "" - CSeq CPSkip p2 -> ppCPhrase p2 - CSeq p1 CPSkip -> ppCPhrase p1 - CSeq p1 p2 -> seq [ppCPhrase p1,ppCPhrase p2] CDo te -> ppTagged te CTrigger vs t -> foreach vs $ ppTerm t CCreate vs t -> "+" ++ foreach vs (ppTerm t) CTerminate vs t -> "-" ++ foreach vs (ppTerm t) CObfuscate vs t -> "~" ++ foreach vs (ppTerm t) CQuery t -> "?" ++ ppTerm t + CPPar p1 p2 -> ppCPhrase p1 ++ ";\n" ++ ppCPhrase p2 CInstQuery b vs t |null vs -> keyw ++ ppTerm t |otherwise -> keyw ++ foreach vs (ppTerm t) where keyw | b = "?--" | otherwise = "?-" - CPDir dir -> case dir of - DirInv ty -> "Invariant " ++ ty ppDecl :: Decl -> String ppDecl td = case td of @@ -209,8 +206,8 @@ StringLit s -> show s Eq t1 t2 -> app_infix "==" (ppTerm t1) (ppTerm t2) Neq t1 t2 -> app_infix "!=" (ppTerm t1) (ppTerm t2) - Exists vs t -> exists vs (ppTerm t) - Forall vs t -> forall vs (ppTerm t) + Exists vs t -> mkexists vs (ppTerm t) + Forall vs t -> mkforall vs (ppTerm t) Count vs t -> "Count" ++ foreach vs (ppTerm t) Sum vs t -> "Sum" ++ foreach vs (ppTerm t) Max vs t -> "Max" ++ foreach vs (ppTerm t) @@ -241,8 +238,8 @@ seq = intercalate ".\n" foreach = binder "Foreach" -exists = binder "Exists" -forall = binder "Forall" +mkexists = binder "Exists" +mkforall = binder "Forall" count = binder "Count" binder :: String -> [Var] -> String -> String diff --git a/src/Language/EFLINT/Saturation.hs b/src/Language/EFLINT/Saturation.hs --- a/src/Language/EFLINT/Saturation.hs +++ b/src/Language/EFLINT/Saturation.hs @@ -6,36 +6,38 @@ import Language.EFLINT.State import Language.EFLINT.Eval -import Control.Monad (forM) +import Control.Monad (foldM) import Control.Applicative (empty) import qualified Data.Map as M import qualified Data.Set as S +-- the monad has been introduced here to propagate missing input exceptions +-- a mechanism is needed to provide input in parallel with declarations +-- to accommodate the situation where a derivation rule is used that interacts with an open type +rebase_and_sat :: Spec -> State -> M_Subs State rebase_and_sat spec = saturate spec . rebase spec rebase :: Spec -> State -> State rebase spec s = s { contents = M.filterWithKey op (contents s) } where op (_,d) i = not (from_sat i) -saturate :: Spec -> State -> State -saturate spec state = case saturate' spec state of - state' | state == state' -> state - | otherwise -> saturate spec state' +saturate :: Spec -> State -> M_Subs State +saturate spec state = saturate' spec state >>= \case + state' | state == state' -> return state + | otherwise -> saturate spec state' where - saturate' spec s = foldl op s (S.toList (derived spec)) + saturate' spec s = foldM op s (S.toList (derived spec)) where op s d = case find_decl spec d of - Nothing -> s - Just tdecl -> foldl clause s (derivation tdecl) + Nothing -> return s + Just tdecl -> foldM clause s (derivation tdecl) where clause s (HoldsWhen t) | Products xs <- domain tdecl = derive xs (When (App d $ Right []) t) s | otherwise = derive [no_decoration d] (When (Ref $ no_decoration d) t) s clause s (Dv xs t) = derive xs t s - where derive xs t s = let dyn = do tes <- foreach xs (whenTagged (eval t) return) - forM tes $ \te -> sat_conditions te >>= \case - True -> return te - False -> empty - ress = case runSubs dyn spec s M.empty M.empty of - Left err -> [] --error ("saturation error:\n" ++ show err) - Right x -> x - in derive_all (concat ress) s + where derive xs t s = let dyn = foreach xs $ + checkFilter sat_conditions (whenTagged (eval t) return) + in case runSubs dyn spec s M.empty of + Left error -> err error + Right ress -> return $ derive_all (concat ress) s + 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 @@ -45,7 +45,7 @@ Just dom -> enumerable spec dom closed_type :: Spec -> DomId -> Maybe Bool -closed_type spec d = fmap closed (find_decl spec d) +closed_type spec d = fmap is_closed (find_decl spec d) type Arguments = Either [Term] [Modifier] @@ -64,10 +64,15 @@ , domain_constraint :: Term , restriction :: Maybe Restriction , derivation :: [Derivation] - , closed :: Bool {- whether closed world assumption is made for this type -} + , closed :: Maybe Bool {- whether closed world assumption is made for this type -} , conditions :: [Term] - } deriving (Eq, Show, Read) + } deriving (Eq, Ord, Show, Read) +is_closed :: TypeSpec -> Bool +is_closed tspec = case closed tspec of + Nothing -> True + Just f -> f + data Derivation = Dv [Var] Term | HoldsWhen Term deriving (Ord, Eq, Show, Read) @@ -93,6 +98,12 @@ } deriving (Ord, Eq, Show, Read) +physical_acts :: Spec -> M.Map DomId TypeSpec +physical_acts = M.filter isPhysical . decls + where isPhysical tspec = case kind tspec of + Act aspec -> physical aspec + _ -> False + data Effect = CAll [Var] Term | TAll [Var] Term | OAll [Var] Term @@ -111,7 +122,7 @@ decls :: M.Map DomId TypeSpec , aliases :: M.Map DomId DomId } - deriving (Eq, Show, Read) + deriving (Eq, Ord, Show, Read) -- | Union of specifications with overrides/replacements, not concretizations spec_union :: Spec -> Spec -> Spec @@ -127,15 +138,11 @@ aliases_union :: M.Map DomId DomId -> M.Map DomId DomId -> M.Map DomId DomId aliases_union old new = M.union new old -actor_ref_address :: String -actor_ref_address = "ref" - emptySpec :: Spec 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) ] basic :: Spec -> S.Set DomId @@ -148,15 +155,8 @@ 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 +restriction_of :: Spec -> DomId -> Maybe Restriction +restriction_of spec d = join $ fmap restriction (M.lookup d (decls spec)) -- type-environment pairs, restricting either: -- * the components of the initial state (all instantiations of restricted by ) @@ -187,6 +187,7 @@ | PQuery Term | PInstQuery Bool {- whether requested instances must hold true -} [Var] Term | PDeclBlock [Decl] + | PParBlock [Phrase] | PSkip deriving (Eq, Show, Read) @@ -200,11 +201,6 @@ | 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) } @@ -219,6 +215,10 @@ | EnforcingActsCl [DomId] | TerminatedByCl [DomId] | CreatedByCl [DomId] + | StringsCl [String] + | IntsCl [Int] + | Close + | Open deriving (Eq, Show, Read) data CModClause = CConditionedByCl [Term] @@ -229,6 +229,10 @@ | CEnforcingActsCl [DomId] | CTerminatedByCl [DomId] | CCreatedByCl [DomId] + | CStringsCl [String] + | CIntsCl [Int] + | CClose + | COpen deriving (Eq, Show, Read) enforcing_act_condition :: DomId {- act id -}-> Term @@ -245,7 +249,13 @@ 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 + where apply_clause clause tspec = case clause of + CClose -> tspec { closed = close (closed tspec) } + where close Nothing = Nothing + close (Just _) = Just True + COpen -> tspec { closed = open (closed tspec) } + where open Nothing = Just False -- by default a type is closed, and can be opened + open (Just f) = Just f -- but once it is closed, it remains closed CConditionedByCl conds -> tspec { conditions = conds ++ conditions tspec } CDerivationCl dvs -> tspec { derivation = dvs ++ derivation tspec } CPostCondCl effs -> tspec { kind = add_effects (kind tspec) } @@ -268,6 +278,14 @@ 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 + CStringsCl ss -> tspec { domain = add_strings (domain tspec) } + where add_strings AnyString = Strings ss + add_strings (Strings ss') = Strings (ss' ++ ss) + add_strings d = d + CIntsCl is -> tspec { domain = add_ints (domain tspec) } + where add_ints AnyInt = Ints is + add_ints (Ints is') = Ints (is' ++ is) + add_ints d = d data CPhrase = CDo Tagged -- execute computed instance | CTrigger [Var] Term -- execute instance to be computed @@ -276,20 +294,9 @@ | CObfuscate [Var] Term | CQuery Term | CInstQuery Bool {- whether generated instances must be present -} [Var] Term - | CPOnlyDecls - | CPDir CDirective - | CSeq CPhrase CPhrase + | CPOnlyDecls -- declarations have been removed during static eval | CPSkip - -data CDirective = DirInv DomId - -process_directives :: [CDirective] -> Spec -> Spec -process_directives = flip (foldr op) - where op (DirInv ty) spec = spec { decls = M.adjust mod ty (decls spec) } - where mod tspec = case kind tspec of - Fact fspec -> tspec { kind = Fact (fspec {invariant = True}) } - _ -> tspec - + | CPPar CPhrase CPhrase invariants :: Spec -> S.Set DomId invariants spec = foldr op S.empty (M.assocs (decls spec)) @@ -523,7 +530,7 @@ , restriction = Nothing , derivation = [] , conditions = [] - , closed = True + , closed = Nothing } int_decl :: TypeSpec @@ -532,7 +539,7 @@ , domain_constraint = BoolLit True , restriction = Nothing , derivation = [] - , closed = True + , closed = Nothing , conditions = [] } ints_decl :: [Int] -> TypeSpec @@ -544,7 +551,7 @@ , domain_constraint = BoolLit True , restriction = Nothing , derivation = [] - , closed = True + , closed = Nothing , conditions = [] } strings_decl :: [String] -> TypeSpec @@ -554,7 +561,7 @@ , domain_constraint = BoolLit True , restriction = Nothing , derivation = [] - , closed = True + , closed = Nothing , conditions = [] } newtype TaggedJSON = TaggedJSON Tagged 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 @@ -1,3 +1,5 @@ +{-# LANGUAGE TupleSections #-} + module Language.EFLINT.State where import Language.EFLINT.Spec @@ -21,12 +23,10 @@ data Transition = Transition { tagged :: Tagged - , exist :: Bool + , exist :: Bool } deriving (Ord, Eq, Show, Read) -type InputMap = M.Map Tagged Bool - type Store = M.Map Tagged Assignment data Assignment = HoldsTrue @@ -34,12 +34,14 @@ | Unknown deriving (Eq, Ord, Show, Read) -emptyInput :: InputMap -emptyInput = M.empty +toAssignment :: Maybe Bool -> Assignment +toAssignment (Just True) = HoldsTrue +toAssignment (Just False) = HoldsFalse +toAssignment Nothing = Unknown emptyStore = M.empty --- | based union over stores, precedence HoldsTrue > HoldsFalse > Unknown +-- | biased union over stores, precedence HoldsTrue > HoldsFalse > Unknown store_union :: Store -> Store -> Store store_union = M.unionWith op where op HoldsTrue _ = HoldsTrue @@ -50,11 +52,18 @@ store_unions :: [Store] -> Store store_unions = foldr store_union emptyStore +missing_assignments :: [Tagged] -> [Tagged] -> [Tagged] -> Maybe Restriction -> MissingInput +missing_assignments trues falses unknowns mres = MissingAssignments (M.unions + [M.fromList $ map (,HoldsTrue) trues + ,M.fromList $ map (,HoldsFalse) falses + ,M.fromList $ map (,Unknown) unknowns]) mres + 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 + where op te@(_,d) HoldsTrue = case restriction_of spec d of + Just VarRestriction -> var_assignment te + Just FunctionRestriction -> function_assignment te + _ -> create te op te HoldsFalse = terminate te op te Unknown = obfuscate te @@ -108,19 +117,19 @@ state_holds :: State -> [Tagged] state_holds state = [ te | (te, m) <- M.assocs (contents state), True == value m ] -state_input_holds :: State -> InputMap -> [Tagged] -state_input_holds state inpm = state_holds state ++ input_holds inpm - state_not_holds :: State -> [Tagged] state_not_holds state = [ te | (te, m) <- M.assocs (contents state), False == value m ] -input_holds :: InputMap -> [Tagged] -input_holds inpm = [ te | (te, True) <- M.assocs inpm ] +assigned_instances :: State -> DomId -> ([Tagged], [Tagged]) +assigned_instances state d = + ([ te | (te@(_,d'), m) <- M.assocs (contents state), d == d', value m == True ] + ,[ te | (te@(_,d'), m) <- M.assocs (contents state), d == d', value m == False ] + ) data Context = Context { - ctx_spec :: Spec --mutable + ctx_spec :: Spec --mutable, fixed? , ctx_state :: State --mutable - , ctx_transitions :: [Transition] -- (label * enabled?) -- replaceable + , ctx_transitions :: [Transition] -- (label * violated?) -- replaceable , ctx_duties :: [Tagged] -- replaceable } @@ -138,7 +147,8 @@ data TransInfo = TransInfo { trans_tagged :: Tagged , trans_assignments :: Store -- includes sync'ed effects - , trans_forced :: Bool -- whether this or a sync'ed transition is not enabled was forced (i.e. was not enabled) + , trans_forced :: Bool -- whether it causes a violation (e.g., is disabled and institutional) + , trans_disabled :: Bool -- whether this, or a sync'ed transition, is not enabled , trans_actor :: Maybe Tagged , trans_syncs :: [TransInfo] -- the transitions this transitions sync'ed with } @@ -167,10 +177,22 @@ deriving (Eq, Ord, Show, Read) data RuntimeError - = MissingInput Tagged + = MissingInput MissingInput | InternalError InternalError deriving (Eq, Ord, Show, Read) +data MissingInput + = MissingAssignments Store (Maybe Restriction) -- all Tagged have same DomId component, complete wrt finite dom + | MissingInstances DomId MDomain (Maybe Restriction) + deriving (Eq, Ord, Show, Read) + +data MDomain = MAnyString + | MAnyInt + | MStrings [String] + | MInts [Int] + | MProducts [(DomId, MDomain)] + deriving (Ord, Eq, Show, Read) + data InternalError = EnumerateInfiniteDomain DomId Domain | MissingSubstitution Var @@ -184,7 +206,9 @@ print_error (RuntimeError err) = print_runtime_error err print_runtime_error :: RuntimeError -> String -print_runtime_error (MissingInput te) = "missing input assignment for: " ++ ppTagged te +print_runtime_error (MissingInput miss) = case miss of + MissingAssignments tes _ -> "missing input assignments for: " ++ show (map ppTagged (M.keys tes)) + MissingInstances domid dom _ -> "missing input assignments for type: " ++ domid print_runtime_error (InternalError err) = "INTERNAL ERROR " ++ print_internal_error err print_internal_error :: InternalError -> String 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 @@ -47,6 +47,16 @@ get_spec :: M_Stc Spec get_spec = M_Stc $ \spec -> Right (spec, spec) +isInitialTypeDecl :: Decl -> Bool +isInitialTypeDecl (TypeDecl _ _) = True +isInitialTypeDecl (TypeExt _ _) = False +isInitialTypeDecl (PlaceholderDecl _ _) = True + +insert_type :: Decl -> M_Stc () +insert_type (TypeDecl d tspec) = insert_typespec d tspec +insert_type (PlaceholderDecl f t) = M_Stc $ \spec -> Right (spec { aliases = M.insert f t (aliases spec) }, ()) +insert_type (TypeExt _ _) = return () + insert_typespec :: DomId -> TypeSpec -> M_Stc () insert_typespec ty tspec = M_Stc $ \spec -> Right (spec { decls = M.insert ty tspec (decls spec) }, ()) @@ -126,13 +136,19 @@ CInstQuery b (vs ++ unbounds) . fst <$> compile_term t PDeclBlock ds -> do -- introduce new types first - let (type_decls, others) = partition isInitialTypeDecl ds - forM_ type_decls (\(TypeDecl d tspec) -> insert_typespec d tspec) + let (inits, others) = partition isInitialTypeDecl ds + forM_ inits insert_type -- then process other type declarations forM_ others $ \decl -> do decls <- compile_decl decl forM_ decls execute_decl - return CPOnlyDecls + return CPOnlyDecls + PParBlock ps -> + let (decls, rest) = foldr sel ([], []) ps -- assumes that operands of ';' do not contain ';' + where sel (PDeclBlock ds) (decls, rest) = (ds ++ decls, rest) + sel phrase (decls, rest) = (decls, phrase:rest) + in compile_phrase (PDeclBlock decls) >>= \case + CPOnlyDecls -> foldr CPPar CPOnlyDecls <$> forM rest compile_phrase where to_stmt (PTrigger vs t) = Trans vs Trigger (Left t) to_stmt (Create vs t) = Trans vs AddEvent (Left t) to_stmt (Terminate vs t) = Trans vs RemEvent (Left t) @@ -175,9 +191,24 @@ 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) + StringsCl ss -> case kind tspec of + Fact _ -> case domain tspec of + AnyString -> return (to_ext ty (CStringsCl ss)) + Strings _ -> return (to_ext ty (CStringsCl ss)) + _ -> err ("cannot extend type " ++ ty ++ "; only string domains can be extended by string literals (Identified by)") + _ -> domain_ext_gen_err + IntsCl is -> case kind tspec of + Fact _ -> case domain tspec of + AnyInt -> return (to_ext ty (CIntsCl is)) + Ints _ -> return (to_ext ty (CIntsCl is)) + _ -> err ("cannot extend type " ++ ty ++ "; only integer domains can be extended by integer literals (Identified by)") + _ -> domain_ext_gen_err + Close -> pure $ to_ext ty CClose + Open -> pure $ to_ext ty COpen where xs = case domain tspec of Products xs -> xs _ -> [no_decoration ty] to_ext ty clause = [CTypeExt ty [clause]] + domain_ext_gen_err = err ("cannot extend type " ++ ty ++ "; only primitive types of kind Fact can have their domain extended (Identified by)") compile_type_spec :: DomId -> TypeSpec -> M_Stc CDecl compile_type_spec ty tspec = do diff --git a/src/REPL.hs b/src/REPL.hs --- a/src/REPL.hs +++ b/src/REPL.hs @@ -15,7 +15,7 @@ import qualified Language.Explorer.Pure as EI -import Control.Monad (forM_, foldM, when, unless) +import Control.Monad (forM_, when, unless) import Control.Monad.Trans.Class (lift) import Data.Char (isSpace) import Data.List (isPrefixOf, isSuffixOf, (\\)) @@ -127,12 +127,12 @@ where continue = repl opts repl_trigger ctx mint = case readMaybe (dropWhile isSpace mint) of Just trig | trig <= length (rest_transitions ctx), trig > 0 - -> repl_phrases opts emptyInput [PDo (fst $ map get_transition (rest_transitions ctx) !! (trig - 1))] exp >>= continue + -> repl_phrases opts [PDo (fst $ map get_transition (rest_transitions ctx) !! (trig - 1))] exp >>= continue _ -> lift display_commands >> continue exp repl_recognize_phrase str = case parse_component syn_phrases str of Left err -> outputStrLn err >> continue exp - Right ps -> repl_phrases opts emptyInput ps exp >>= continue + Right ps -> repl_phrases opts ps exp >>= continue revert_or_jump destr mint sid = case readMaybe (dropWhile isSpace mint) of Just sid' -> case run_ exp (Revert sid' destr) of @@ -146,14 +146,14 @@ repl_directive_phrases opts (edp:ps) explorer = case edp of Left d -> repl_directive opts d explorer >>= repl_directive_phrases opts ps - Right p -> repl_phrases opts emptyInput [p] explorer >>= repl_directive_phrases opts ps + Right p -> repl_phrases opts [p] explorer >>= repl_directive_phrases opts ps where (_,_,(_,ctx)) = get_last_edge explorer (EI.currRef explorer) isQuery phrase = case phrase of PQuery _ -> True _ -> False -repl_phrases :: Options -> InputMap -> [Phrase] -> Explorer -> InputT IO Explorer -repl_phrases opts inpm phrases explorer = - repl_report opts inpm phrases (run_ explorer (Execute (convert_programs phrases) inpm)) explorer +repl_phrases :: Options -> [Phrase] -> Explorer -> InputT IO Explorer +repl_phrases opts phrases explorer = + repl_report opts phrases (run_ explorer (Execute (convert_programs phrases))) explorer repl_directive :: Options -> Directive -> Explorer -> InputT IO Explorer repl_directive opts (Include fp) explorer = repl_import opts fp explorer @@ -188,28 +188,26 @@ | otherwise = return (Left (show exc)) -repl_report :: Options -> InputMap -> [Phrase] -> -- both used for re-execution in case of missing input +repl_report :: Options -> [Phrase] -> -- both used for re-execution in case of missing input Response -> Explorer -> InputT IO Explorer -repl_report opts inpm phrases res exp = case res of +repl_report opts phrases res exp = case res of ResultTrans exp outs (old,_) (ctx,sid) -> case missing_inputs outs of [] -> 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 - where consider Nothing _ = return Nothing - consider (Just inpm) te@(_,d) = do - mass <- lift (consume_input opts) - let tryWith b = Just $ M.insert te b inpm - case mass of - Just b -> return (tryWith b) - Nothing -> do + ms -> do forM_ (missing_instances_for ms) $ \(d,dom,_) -> + lift (putStrLn ("missing input assignments for type: " ++ d)) + let missing_tes = concatMap op ms + where op (MissingAssignments sto _) = [ te | (te, Unknown) <- M.assocs sto ] + op (MissingInstances _ _ _) = [] + forM_ missing_tes $ \te -> lift $ putStrLn ("\nmissing truth-value for: " ++ ppTagged te) - lift $ putStrLn ("is this fact True or False?") - getInputLine "(True/False) > " >>= \case - Just s -> return $ tryWith (readAssignmentMaybe s) - Nothing -> return Nothing + return exp InvalidRevert -> error "REPL.assert 1" +missing_input :: [MissingInput] -> [Tagged] +missing_input = concatMap op + where op (MissingAssignments tes _) = [ te | (te,Unknown) <- M.assocs tes ] + op (MissingInstances d dom _) = [] + display_commands = putStrLn "Available commands:\n\ \ : same as :choose \n\ @@ -289,8 +287,8 @@ where display_triggers' [] = putStrLn ("no " ++ str ++ "actions or events") display_triggers' tes = putStrLn (str ++ "actions & events:") >> mapM_ op (zip [1..] tes) where op (i, (te,en)) = putStrLn (show i ++ ". " ++ ppTagged te ++ enabled) - where enabled | en = " (ENABLED)" - | otherwise = " (DISABLED)" + where enabled | en = " (PERMITTED)" + | otherwise = " (PROHIBITED)" display :: Config -> IO () display cfg = putStrLn (show (cfg_state cfg)) diff --git a/src/Server.hs b/src/Server.hs --- a/src/Server.hs +++ b/src/Server.hs @@ -2,10 +2,11 @@ {-# LANGUAGE RecordWildCards, DuplicateRecordFields #-} import Language.EFLINT.Spec hiding (Value(..)) -import Language.EFLINT.State +import Language.EFLINT.State as State import Language.EFLINT.Util import Language.EFLINT.Options import Language.EFLINT.StaticEval +import Language.EFLINT.FormExtraction import Language.EFLINT.Parse import Language.EFLINT.Print (ppProgram) import Language.EFLINT.Explorer hiding (Instruction(Revert), Response) @@ -75,7 +76,7 @@ Right p -> run_phrase opts p (run_directives_phrases opts ps cont) exp run_phrase :: Options -> Phrase -> Cont a -> Cont a -run_phrase opts phrase cont exp = case run_ exp (Execute (convert_programs [phrase]) emptyInput) of +run_phrase opts phrase cont exp = case run_ exp (Execute (convert_programs [phrase])) of ResultTrans exp _ _ _ -> cont exp Path _ -> putStrLn "Unexpected execution path encountered" >> cont exp Nodes _ -> putStrLn "Unexpected collection of nodes encountered" >> cont exp @@ -141,14 +142,14 @@ string <- hGetLine handle let (_, _, (sid, ctx)) = get_last_edge exp (EI.currRef exp) putStrLn string - let compile_and inpm program = report $ run_ exp (Execute [program] inpm) + let compile_and program = report $ run_ exp (Execute [program]) report res = case res of ResultTrans exp outs (old,oid) (new,sid) -> report_success sock outs oid old sid new exp Path path -> do hPutStrLn handle (json_encode (GivePath path)) hClose handle continue sock exp --- Explorer.ExecError err -> report_error (ExecError err) exp +-- Explorer.ExecError err -> report_json (ExecError err) exp Nodes nodes -> do hPutStrLn handle (json_encode (GiveNodes nodes)) hClose handle @@ -163,8 +164,8 @@ hPutStrLn handle (json_encode (GiveLoadGraph)) hClose handle continue sock exp - InvalidRevert -> report_error InvalidState exp --- CompilationError err -> report_error (InvalidInput err) exp + InvalidRevert -> report_json InvalidState exp +-- CompilationError err -> report_json (InvalidInput err) exp report_success sock outputs old_id c0 state_id ctx exp = do let facts_from = state_holds (cfg_state c0) let facts_to = state_holds (cfg_state ctx) @@ -191,85 +192,97 @@ new_duties term_duties all_duties new_enabled new_disabled transitions ms -> InputRequired ms - hPutStrLn handle (json_encode response) + report_json response exp hClose handle continue sock exp - report_error err exp = do - hPutStrLn handle (json_encode err) + report_json response exp = do + hPutStrLn handle (json_encode response) hClose handle continue sock exp let withCommand cmd = case cmd of - 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) + CreateEvent term -> compile_and $ Program (Create [] term) + TerminateEvent term -> compile_and $ Program (Terminate [] term) + QueryCommand term -> compile_and $ Program (PQuery term) 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 CreateExport -> report $ run_ exp CreateExportExploration LoadExport graph -> report $ run_ exp (LoadExportExploration graph) - GetFacts inpm -> do hPutStrLn handle (json_encode (GiveFacts (state_input_holds (cfg_state ctx) inpm))) + GetFacts -> do hPutStrLn handle (json_encode (GiveFacts (state_holds (cfg_state ctx)))) hClose handle continue sock exp + GetTypes -> hPutStrLn handle (json_encode (GiveTypes (decls (cfg_spec ctx)))) >> hClose handle >> continue sock exp + GetPhysicalActs -> hPutStrLn handle (json_encode (GiveTypes (physical_acts (cfg_spec ctx)))) >> hClose handle >> continue sock exp Kill -> hPutStrLn handle (json_encode ByeBye) >> hClose handle - ActionCommand d a r os force inpm -> compile_and inpm $ Program (PTrigger [] term) + ActionCommand d a r os force -> compile_and $ Program (PTrigger [] term) where term = App d (Left (a : r : os)) - CmdTrigger t b inpm -> compile_and inpm (Program (PTrigger [] t)) - Phrase str inpm -> case parse_component syn_phrases str of + CmdTrigger t b -> compile_and (Program (PTrigger [] t)) + RequestInputRequired mphrase -> flip report_json exp $ case mphrase of + Nothing -> InputRequired $ S.toList $ form_all_open spec state + Just str -> case parse_component syn_phrases str of + Left err -> InvalidInput err + Right ps -> InputRequired $ S.toList $ form_from_phrases ps spec state + where spec = cfg_spec $ EI.config exp + state = cfg_state $ EI.config exp + Phrase str -> case parse_component syn_phrases str of Left err -> do hPutStrLn handle (json_encode (InvalidInput err)) hClose handle >> continue sock exp - Right ps -> report $ run_ exp (Execute (convert_programs ps) inpm) - Phrases str inpm -> case parse_component syn_phrases str of + Right ps -> report $ run_ exp (Execute (convert_programs ps)) + Phrases str -> case parse_component syn_phrases str of Left err -> do hPutStrLn handle (json_encode (InvalidInput err)) hClose handle >> continue sock exp - Right ps -> report $ run_ exp (ExecuteOnce (collapse_programs (convert_programs ps)) inpm) + Right ps -> report $ run_ exp (ExecuteOnce (collapse_programs (convert_programs ps))) case eitherDecode (Data.ByteString.Lazy.Char8.pack string) of Left err -> do when (find debug opts) (putStrLn err) case (find accept_phrases opts) of False -> do hPutStrLn handle (json_encode (InvalidCommand err)) hClose handle continue sock exp - True -> withCommand (Phrase string emptyInput) + True -> withCommand (Phrase string) Right cmd-> withCommand cmd json_encode r = Data.ByteString.Lazy.Char8.unpack (encode r) -data Command = ActionCommand DomId Term Term [Term] Bool InputMap - | CmdTrigger Term Bool InputMap - | CreateEvent Term InputMap - | TerminateEvent Term InputMap - | QueryCommand Term InputMap +data Command = ActionCommand DomId Term Term [Term] Bool + | CmdTrigger Term Bool + | CreateEvent Term + | TerminateEvent Term + | QueryCommand Term | Revert Int Bool {- whether the revert is destructive or not -} | Status (Maybe Int) | Kill - | GetFacts InputMap + | GetFacts + | GetTypes + | GetPhysicalActs | History (Maybe Int) | Heads | CreateExport | LoadExport ExecutionGraph - | Phrase String InputMap - | Phrases String InputMap + | Phrase String + | Phrases String + | RequestInputRequired (Maybe String) {- phrase -} instance FromJSON Command where parseJSON = withObject "Command" $ \v -> do cmd <- v .: "command" case cmd::String of - "create" -> CreateEvent . value_to_term <$> v .: "value" <*> maybe_input v - "terminate" -> TerminateEvent . value_to_term <$> v .: "value" <*> maybe_input v - "test-present"-> QueryCommand . value_to_term <$> v .: "value" <*> maybe_input v + "create" -> CreateEvent . value_to_term <$> v .: "value" + "terminate" -> TerminateEvent . value_to_term <$> v .: "value" + "test-present"-> QueryCommand . value_to_term <$> v .: "value" - "test-absent" -> QueryCommand . Not . value_to_term <$> v .: "value" <*> maybe_input v + "test-absent" -> QueryCommand . Not . value_to_term <$> v .: "value" - "enabled" -> QueryCommand . Enabled . value_to_term <$> v .: "value" <*> maybe_input v + "enabled" -> QueryCommand . Enabled . value_to_term <$> v .: "value" "revert" -> Revert <$> v .: "value" <*> (v .: "destructive" <|> return False) "action" -> full_action <|> trigger_action where full_action = actionCommand <$> v .: "act-type" <*> v .: "actor" <*> v .: "recipient" - <*> v .: "objects" <*> maybe_force v <*> maybe_input v - trigger_action = CmdTrigger . value_to_term <$> v .: "value" <*> maybe_force v <*> maybe_input v + <*> v .: "objects" <*> maybe_force v + trigger_action = CmdTrigger . value_to_term <$> v .: "value" <*> maybe_force v actionCommand d a r os = ActionCommand d (to_term a) (to_term r) (map to_term os) "status" -> Status <$> v .: "state" <|> return (Status Nothing) @@ -279,25 +292,35 @@ "create-export" -> return CreateExport "load-export" -> LoadExport <$> v .: "graph" "kill" -> return Kill - "phrase" -> Phrase <$> v .: "text" <*> maybe_input v - "phrases" -> Phrases <$> v .: "text" <*> maybe_input v - "event" -> CmdTrigger . value_to_term <$> v .: "value" <*> maybe_force v <*> maybe_input v - "facts" -> GetFacts <$> maybe_input v + "phrase" -> Phrase <$> v .: "text" + "phrases" -> Phrases <$> v .: "text" + "event" -> CmdTrigger . value_to_term <$> v .: "value" <*> maybe_force v + "facts" -> return GetFacts + "types" -> return GetTypes + "physical-acts" -> return GetPhysicalActs + "input required" -> RequestInputRequired <$> maybe_phrase v _ -> mzero +maybe_phrase v = Just <$> v .: "phrase" <|> pure Nothing maybe_force v = v .: "force" <|> return False -maybe_input v = value_based_input <$> v .: "input" <|> return emptyInput -value_based_input :: [AssTuple] -> InputMap -value_based_input = M.fromList . map toTup - where toTup at = (value_to_tagged $ (value :: AssTuple -> Value) at, assignment at) - encode_store :: Store -> [AssTuple] encode_store = concatMap toTup . M.assocs where toTup (te, HoldsTrue) = return $ AssTuple (tagged_to_value te) True toTup (te, HoldsFalse) = return $ AssTuple (tagged_to_value te) False toTup (te, Unknown) = [] +-- data TaggedInput = TaggedInput { name :: DomId +-- , assignments :: [OptAssTuple] } deriving (Generic) +-- instance FromJSON TaggedInput +-- instance ToJSON TaggedInput +-- +data OptAssTuple = OptAssTuple { value :: Value + , opt_assignment :: Maybe Bool } deriving (Generic) +instance FromJSON OptAssTuple +instance ToJSON OptAssTuple + + data AssTuple = AssTuple { value :: Value , assignment :: Bool } deriving (Generic) instance FromJSON AssTuple where @@ -375,7 +398,8 @@ (S.Set Tagged) -- newly disabled transitions (S.Set Transition) -- all transitions | InvalidState - | InputRequired [Tagged] + | InputRequired [MissingInput] + | GiveTypes (M.Map DomId TypeSpec) | GiveFacts [Tagged] | GivePath Path | GiveNodes [Node] @@ -384,7 +408,7 @@ | ByeBye instance ToJSON Response where - toJSON (InputRequired tes) = object [ "response" .= JSON.String "input required", "values" .= toJSON (map tagged_to_value tes)] + toJSON (InputRequired miss) = object [ "response" .= JSON.String "input required", "values" .= toJSON miss] 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 @@ -419,6 +443,7 @@ toJSON (InvalidInput err) = object [ "response" .= JSON.String "invalid input" , "error" .= toJSON err ] toJSON ByeBye = object [ "response" .= JSON.String "bye world.." ] + toJSON (GiveTypes m) = object [ "types" .= toJSON m ] toJSON (GiveFacts tes) = object [ "values" .= toJSON (map TaggedJSON tes) ] toJSON (GiveNodes nodes) = object [ "nodes" .= toJSON (map toJSONNode nodes) ] where toJSONNode (sid, cfg) = @@ -437,8 +462,7 @@ toJSON (GivePath edges) = object [ "edges" .= toJSON (map toJSONEdge edges') ] where edges' = sortBy (on compare (\((sid,_),_,_) -> sid)) edges toJSONEdge ((sid_from,ctx_from), (phr, output), (sid_to, ctx_to)) = - object [ "phrase" .= toJSON (ppProgram (snd phr)) - , "input" .= toJSON (fst phr) + object [ "phrase" .= toJSON (ppProgram phr) , "source_id" .= toJSON sid_from , "target_id" .= toJSON sid_to @@ -520,9 +544,9 @@ ,"value" .= d ] CompilationError err -> object ["error-type" .= JSON.String "compilation error" ,"error" .= toJSON err] - RuntimeError (MissingInput te) -> + RuntimeError (MissingInput miss) -> object ["error-type" .= JSON.String "missing input" - ,"error" .= JSON.toJSON (TaggedJSON te) ] + ,"error" .= JSON.toJSON miss ] RuntimeError (InternalError (EnumerateInfiniteDomain d dom)) -> object ["error-type" .= JSON.String "enumerating infinite domain" ,"error" .= toJSON (d, dom) ] @@ -545,6 +569,24 @@ _ -> fail ("unknown type: " ++ errortype) +instance ToJSON MissingInput where + toJSON err = case err of + MissingAssignments tes mres -> + object ( ["input-type" .= JSON.String "assignments" + ,"value" .= JSON.toJSON (map toAssTuple (M.assocs tes)) ] + ++ maybe [] ((:[]) . ("restriction" .=) . toJSON) mres) + where toAssTuple (te, HoldsTrue) = OptAssTuple (tagged_to_value te) (Just True) + toAssTuple (te, HoldsFalse) = OptAssTuple (tagged_to_value te) (Just False) + toAssTuple (te, Unknown) = OptAssTuple (tagged_to_value te) Nothing + MissingInstances d dom mres -> + object (["input-type" .= JSON.String "instances" + ,"value" .= d + ,"domain" .= toJSON dom ] ++ maybe [] ((:[]) . ("restriction" .=) . toJSON) mres) + +instance ToJSON Restriction where + toJSON VarRestriction = "var" + toJSON FunctionRestriction = "function" + instance ToJSON Output where toJSON (ExecutedTransition info) = object [ "output-type" .= JSON.String "executed-transition", "info" .= toJSON info] toJSON (Violation v) = object [ "output-type" .= JSON.String "violation", "output" .= v] @@ -621,7 +663,7 @@ instance ToJSON Info where toJSON info = object [ - "value" .= toJSON ((value :: Info -> Bool) info ), + "value" .= toJSON ((State.value :: Info -> Bool) info ), "from-sat" .= toJSON (from_sat info) ] @@ -920,6 +962,13 @@ toJSON (Products vars) = object ["domain-type" .= JSON.String "Products", "vars" .= vars] toJSON (Time) = object ["domain-type" .= JSON.String "Time"] +instance ToJSON MDomain where + toJSON (MAnyString) = object ["domain-type" .= JSON.String "AnyString"] + toJSON (MAnyInt) = object ["domain-type" .= JSON.String "AnyInt"] + toJSON (MStrings strings) = object ["domain-type" .= JSON.String "Strings", "strings" .= strings] + toJSON (MInts ints) = object ["domain-type" .= JSON.String "Ints", "ints" .= ints] + toJSON (MProducts vars) = object ["domain-type" .= JSON.String "Products", "vars" .= vars] + instance FromJSON Domain where parseJSON = withObject "anystring or anyint or strings or ints or products or time or external" $ \o -> do domaintype <- o .: "domain-type" @@ -973,6 +1022,7 @@ TransInfo <$> o .: "trans-tagged" <*> o .: "trans-assignments" <*> o .: "trans-forced" + <*> o .: "trans-disabled" <*> o .: "trans-actor" <*> o .: "trans-syncs" @@ -1035,8 +1085,7 @@ -- TODO remove show and use ToJSON functions instance ToJSON PO where toJSON po = object [ - "program" .= ppProgram (snd $ label po), - "input" .= show (fst $ label po), + "program" .= ppProgram (label po), "output" .= show (output po) ] @@ -1045,9 +1094,7 @@ parseJSON = withObject "label output" $ \o -> do program_show <- o .: "label" output_show <- o .: "output" - input_show <- o .: "input" let output = read output_show - let input = read input_show case parse_component syn_phrases program_show of Left err -> error(err) - Right ps -> return PO{label=(input, collapse_programs (convert_programs ps)),..} + Right ps -> return PO{label=(collapse_programs (convert_programs ps)),..}