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.1 +version: 3.0.0.2 synopsis: Simulation interpreter for FLINT policy descriptions description: @@ -42,7 +42,7 @@ Language.EFLINT.Interpreter Language.EFLINT.Util Language.EFLINT.Options - build-depends: base >=4.9 && <= 4.14.1 + build-depends: base >=4.9 && < 4.15 , containers >=0.5 && <0.7 , hxt >= 9.3.1.16 , time >= 1.8.0.2 @@ -76,7 +76,7 @@ Language.EFLINT.Interpreter Language.EFLINT.Util Language.EFLINT.Options - build-depends: base >=4.9 && <= 4.14.1 + build-depends: base >=4.9 && < 4.15 , containers >=0.5 && <0.7 , hxt >= 9.3.1.16 , time >= 1.8.0.2 @@ -111,7 +111,7 @@ Language.EFLINT.JSON Language.EFLINT.Util Language.EFLINT.Options - build-depends: base >=4.9 && <= 4.14.1 + build-depends: base >=4.9 && < 4.15 , containers >=0.5 && <0.7 , hxt >= 9.3.1.16 , time >= 1.8.0.2 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 @@ -255,8 +255,8 @@ Fact _ -> empty Duty _ -> empty Act aspec -> do_transition te actor is_enabled (effects aspec) (syncs aspec) - Event espec -> do_transition te actor is_enabled (event_effects espec) [] - where do_transition te@(v,d) isAction is_enabled effects ss = do + Event espec -> do_transition te Nothing is_enabled (event_effects espec) [] + where do_transition te@(v,d) mActor is_enabled effects ss = do (dom, _) <- get_dom d let Products xs = dom let Product args = v @@ -265,7 +265,7 @@ 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) isAction sync_infos) + return (TransInfo te ass (any_f || not is_enabled) mActor sync_infos) actor = case v of Product (a:objs) -> Just a _ -> Nothing 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 @@ -11,7 +11,7 @@ import Language.EFLINT.StaticEval (compile_phrase, runStatic) import Language.EFLINT.State -import Control.Monad (forM, when) +import Control.Monad (forM, forM_, when) import Control.Monad.Writer (Writer, tell, runWriter) import Control.Applicative (empty) @@ -125,9 +125,13 @@ 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 . (:[])) - CTrigger vs t -> let m_subs = do tes <- foreach vs (whenTagged (eval t) return) - forM tes trigger_or_fail + CDo te -> error_or_process (trigger_or_fail te) spec state inpm 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) @@ -159,22 +163,17 @@ error_or_process (eval_effect eff) spec state inpm $ \stores -> return_context (M.unions stores) {- always just one store-} [] - trigger_or_fail :: Tagged -> M_Subs (Either Tagged TransInfo) - trigger_or_fail te@(_,d) | triggerable spec d = Right <$> instantiate_trans te - | otherwise = return $ Left te - - consider_transinfos infos = case infos of - [[Left te]] -> tell [ErrorVal (NotTriggerable te)] >> no_effect - [[Right info]] -> report_on_trans info - _ -> tell [ErrorVal NonDeterministicTransition] >> no_effect - + trigger_or_fail :: Tagged -> M_Subs (Either DomId [TransInfo]) + trigger_or_fail te@(_,d) | triggerable spec d = Right . (:[]) <$> instantiate_trans te + | otherwise = return $ Left d - report_on_trans :: TransInfo -> OutputWriter (Maybe Context) - report_on_trans info = do - tell [ExecutedTransition info] - when (trans_is_action info && trans_forced info) - (tell [Violation (TriggerViolation info)]) - return_context (trans_assignments info) [] + 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)]) + return_context (store_unions (map trans_assignments infos)) [] + consider_transinfos _ = error "ASSERT: consider_transinfos" find_inv_violations :: [DomId] -> M_Subs [Violation] find_inv_violations ds = do 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 @@ -141,6 +141,10 @@ trans_is_action :: TransInfo -> Bool trans_is_action = isJust . trans_actor +-- | Get all the TransInfo nodes in the tree represented by the given root +trans_all_infos :: TransInfo -> [TransInfo] +trans_all_infos info = info : concatMap trans_all_infos (trans_syncs info) + data Violation = DutyViolation Tagged | TriggerViolation TransInfo | InvariantViolation DomId @@ -151,8 +155,7 @@ deriving (Ord, Eq, Show, Read) data Error = -- trigger errors - NotTriggerable Tagged - | NonDeterministicTransition + NotTriggerable DomId | CompilationError String | RuntimeError RuntimeError deriving (Eq, Ord, Show, Read) @@ -170,8 +173,7 @@ deriving (Eq, Ord, Show, Read) print_error :: Error -> String -print_error (NotTriggerable te) = "not a triggerable instance: " ++ ppTagged te -print_error (NonDeterministicTransition) = "non-deterministic transition attempt" +print_error (NotTriggerable d) = "not a triggerable (act- or event-) type: " ++ d print_error (CompilationError err) = err print_error (RuntimeError err) = print_runtime_error err 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 @@ -391,9 +391,9 @@ return (Neq t1' t2', TyBool)) Count xs t -> do (t', tau) <- compile_term t return (Count xs t', TyInts) - Max xs t -> do (t', tau) <- compile_term t + Max xs t -> do t' <- convert_term t TyInts return (Max xs t', TyInts) - Min xs t -> do (t', tau) <- compile_term t + Min xs t -> do t' <- convert_term t TyInts return (Min xs t', TyInts) When t1 t2 -> do (t1', tau) <- compile_term t1 t2' <- convert_term t2 TyBool diff --git a/src/Server.hs b/src/Server.hs --- a/src/Server.hs +++ b/src/Server.hs @@ -508,9 +508,8 @@ instance ToJSON Error where toJSON err = case err of - NonDeterministicTransition -> object [ "error-type" .= JSON.String "non-deterministic transition"] - NotTriggerable te -> object ["error-type" .= JSON.String "not triggerable" - ,"value" .= TaggedJSON te ] + NotTriggerable d -> object ["error-type" .= JSON.String "not triggerable" + ,"value" .= d ] CompilationError err -> object ["error-type" .= JSON.String "compilation error" ,"error" .= toJSON err] RuntimeError (MissingInput te) -> @@ -530,10 +529,9 @@ ,"error" .= d ] instance FromJSON Error where - parseJSON = withObject "NonDeterministicTransition or NotTriggerable or CompilationError" $ \o -> do + parseJSON = withObject "NotTriggerable or CompilationError" $ \o -> do errortype <- o .: "error-type" case errortype of - "non-deterministic transition" -> return NonDeterministicTransition "not triggerable" -> NotTriggerable <$> o .: "value" "compilation error" -> CompilationError <$> o .: "error" _ -> fail ("unknown type: " ++ errortype)