eflint 3.0.0.1 → 3.0.0.2

raw patch · 6 files changed

+36/−37 lines, 6 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• eflint.cabal +4/−4
• src/Language/EFLINT/Eval.hs +3/−3
• src/Language/EFLINT/Interpreter.hs +18/−19
• src/Language/EFLINT/State.hs +6/−4
• src/Language/EFLINT/StaticEval.hs +2/−2
• src/Server.hs +3/−5

@@ -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

@@ -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 

@@ -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 

@@ -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 

@@ -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

@@ -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)