eflint 3.1.0.1 → 3.1.0.2
raw patch · 5 files changed
+15/−8 lines, 5 files
Files
- eflint.cabal +2/−2
- src/Language/EFLINT/Interpreter.hs +2/−2
- src/Language/EFLINT/Options.hs +3/−1
- src/REPL.hs +1/−1
- src/Server.hs +7/−2
eflint.cabal view
@@ -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
src/Language/EFLINT/Interpreter.hs view
@@ -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
src/Language/EFLINT/Options.hs view
@@ -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 })
src/REPL.hs view
@@ -214,7 +214,7 @@ putStrLn "Available commands:\n\ \ :<INT> same as :choose <INT>\n\ \ :choose <INT> choose action or event trigger <INT>\n\- \ :force <INT> choose and force action or event trigger <INT>\n\+ \ :jump <INT> jump to the configuration with id <INT>\n\ \ :revert <INT> revert to the configuration with id <INT>\n\ \ :display :d show all contents of the current configuration\n\ \ :spec pretty-print all type definitions\n\
src/Server.hs view
@@ -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