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.1.0.1 +version: 3.1.0.2 synopsis: Simulation interpreter for FLINT policy descriptions description: @@ -103,10 +103,10 @@ , Language.EFLINT.Print , Language.EFLINT.Interpreter , Language.EFLINT.Explorer + , Language.EFLINT.Saturation other-modules: Language.EFLINT.StaticEval Language.EFLINT.Eval - Language.EFLINT.Saturation Language.EFLINT.Binders Language.EFLINT.JSON Language.EFLINT.Util 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 @@ -198,7 +198,7 @@ find_inv_violations :: [DomId] -> M_Subs [Violation] find_inv_violations ds = do spec <- get_spec - forM ds $ \d -> do + (concat <$>) $ forM ds $ \d -> results $ do let term = Exists [Var d ""] (Present (Ref (Var d ""))) ignoreMissingInput (checkFalse (eval term)) return (InvariantViolation d) @@ -206,7 +206,7 @@ find_duty_violations :: [Tagged] -> M_Subs [Violation] find_duty_violations tes = do spec <- get_spec - forM tes $ \te@(_,d) -> do + (concat <$>) $ forM tes $ \te@(_,d) -> results $ do ignoreMissingInput (eval_violation_condition te (find_violation_cond spec d)) >>= \case True -> return (DutyViolation te) False -> empty diff --git a/src/Language/EFLINT/Options.hs b/src/Language/EFLINT/Options.hs --- a/src/Language/EFLINT/Options.hs +++ b/src/Language/EFLINT/Options.hs @@ -76,9 +76,11 @@ has_been_included file opts = unsafePerformIO $ do dirs <- include_paths <$> readIORef opts files <- included_files <$> readIORef opts + files' <- mapM canonicalizePath files find_included_file dirs file >>= \case [] -> return False - (file:_) -> return (file `elem` files) + (file:_) -> (`elem` files') <$> canonicalizePath file + add_filepath :: FilePath -> Options -> IO () add_filepath fp opts = do modifyIORef opts (\os -> os { filepath = Just fp }) diff --git a/src/REPL.hs b/src/REPL.hs --- a/src/REPL.hs +++ b/src/REPL.hs @@ -214,7 +214,7 @@ putStrLn "Available commands:\n\ \ : same as :choose \n\ \ :choose choose action or event trigger \n\ - \ :force choose and force action or event trigger \n\ + \ :jump jump to the configuration with id \n\ \ :revert revert to the configuration with id \n\ \ :display :d show all contents of the current configuration\n\ \ :spec pretty-print all type definitions\n\ diff --git a/src/Server.hs b/src/Server.hs --- a/src/Server.hs +++ b/src/Server.hs @@ -179,6 +179,7 @@ let transitions = S.fromList (rest_transitions ctx) let new_duties = S.fromList (rest_duties ctx) S.\\ S.fromList (rest_duties c0) + let term_duties = S.fromList (rest_duties c0) S.\\ S.fromList (rest_duties ctx) let new_enabled = S.fromList (rest_enabled ctx) S.\\ S.fromList (rest_enabled c0) let new_disabled = S.fromList (rest_disabled ctx) S.\\ S.fromList (rest_disabled c0) let all_duties = S.fromList $ rest_duties ctx @@ -187,7 +188,7 @@ [] -> CommandSuccess old_id state_id facts_from facts_to created_facts terminated_facts viols outs errs qress iqress - new_duties all_duties + new_duties term_duties all_duties new_enabled new_disabled transitions ms -> InputRequired ms hPutStrLn handle (json_encode response) @@ -368,6 +369,7 @@ [QueryRes] -- query results [[Tagged]] -- instance query results (S.Set Tagged) -- new duties + (S.Set Tagged) -- terminated duties (S.Set Tagged) -- all duties in the current state (S.Set Tagged) -- newly enabled transitions (S.Set Tagged) -- newly disabled transitions @@ -387,7 +389,7 @@ toJSON (CommandSuccess sid_from i facts_from facts_to created_facts terminated_facts vs outs errs qress iqress - new_duties all_duties + new_duties term_duties all_duties new_enabled new_disabled all_transitions) = object [ "response" .= JSON.String "success" , "old-state" .= toJSON sid_from @@ -404,6 +406,7 @@ , "inst-query-results" .= toJSON (map TaggedJSON (concat iqress)) , "new-duties" .= toJSON (map TaggedJSON $ S.toList new_duties) + , "terminated-duties" .= toJSON (map TaggedJSON $ S.toList term_duties) , "new-enabled-transitions" .= toJSON (map TaggedJSON $ S.toList new_enabled) , "new-disabled-transitions" .= toJSON (map TaggedJSON $ S.toList new_disabled) , "all-duties" .= toJSON (map TaggedJSON $ S.toList all_duties) @@ -450,6 +453,7 @@ , "query-results" .= toJSON qress , "new-duties" .= toJSON (map TaggedJSON $ S.toList new_duties) + , "terminated-duties" .= toJSON (map TaggedJSON $ S.toList term_duties) , "new-enabled-transitions" .= toJSON (map TaggedJSON $ S.toList new_enabled) , "new-disabled-transitions" .= toJSON (map TaggedJSON $ S.toList new_disabled) , "all-duties" .= toJSON (map TaggedJSON $ S.toList all_duties) @@ -470,6 +474,7 @@ en_transitions = map fst $ filter snd $ map get_transition (S.toList all_transitions) dis_transitions = map fst $ filter (not . snd) $ map get_transition (S.toList all_transitions) new_duties = S.fromList (rest_duties ctx_to) S.\\ S.fromList (rest_duties ctx_from) + term_duties = S.fromList (rest_duties ctx_from) S.\\ S.fromList (rest_duties ctx_to) new_enabled = S.fromList (rest_enabled ctx_to) S.\\ S.fromList (rest_enabled ctx_from) new_disabled = S.fromList (rest_disabled ctx_to) S.\\ S.fromList (rest_disabled ctx_from) all_duties = S.fromList $ rest_duties ctx_to