d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson{- |

d49d75f5073294d798aa500728116309398bb535Andreas GustafssonModule : $Header$

800f99741c01cfb1b9a0294688349398bc8a0271Automatic UpdaterCopyright : (c) Christian Maeder, Uni Bremen 2004

dafcb997e390efa4423883dafd100c975c4095d6Mark AndrewsLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

40f53fa8d9c6a4fc38c0014495e7a42b08f52481David Lawrence

ec5347e2c775f027573ce5648b910361aa926c01Automatic UpdaterMaintainer : hets@tzi.de

d49d75f5073294d798aa500728116309398bb535Andreas GustafssonStability : provisional

d49d75f5073294d798aa500728116309398bb535Andreas GustafssonPortability : portable

40f53fa8d9c6a4fc38c0014495e7a42b08f52481David Lawrence

dafcb997e390efa4423883dafd100c975c4095d6Mark Andrewsstatic analysis of modal logic parts

dafcb997e390efa4423883dafd100c975c4095d6Mark Andrews-}

dafcb997e390efa4423883dafd100c975c4095d6Mark Andrews

dafcb997e390efa4423883dafd100c975c4095d6Mark Andrews{- todo:

dafcb997e390efa4423883dafd100c975c4095d6Mark Andrews check quantifiers (sorts, variables in body) in ana_M_FORMULA

dafcb997e390efa4423883dafd100c975c4095d6Mark Andrews-}

dafcb997e390efa4423883dafd100c975c4095d6Mark Andrews

d49d75f5073294d798aa500728116309398bb535Andreas Gustafssonmodule Modal.StatAna where

ea94d370123a5892f6c47a97f21d1b28d44bb168Tinderbox User

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson--import Debug.Trace

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson

d49d75f5073294d798aa500728116309398bb535Andreas Gustafssonimport Modal.AS_Modal

eefe56c8b367d1e54361b0c55f9db9d9468a0d6aAndreas Gustafssonimport Modal.Print_AS

d49d75f5073294d798aa500728116309398bb535Andreas Gustafssonimport Modal.ModalSign

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafsson

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafssonimport CASL.Sign

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafssonimport CASL.MixfixParser

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafssonimport CASL.StaticAna

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafssonimport CASL.AS_Basic_CASL

d49d75f5073294d798aa500728116309398bb535Andreas Gustafssonimport CASL.Overload

d49d75f5073294d798aa500728116309398bb535Andreas Gustafssonimport CASL.MapSentence

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrewsimport Common.AS_Annotation

683e751c957d8b209cc393ff603bea937f5565b0Mark Andrewsimport qualified Common.Lib.Set as Set

683e751c957d8b209cc393ff603bea937f5565b0Mark Andrewsimport Common.Lib.State

683e751c957d8b209cc393ff603bea937f5565b0Mark Andrewsimport Common.Id

683e751c957d8b209cc393ff603bea937f5565b0Mark Andrewsimport Common.Result

683e751c957d8b209cc393ff603bea937f5565b0Mark Andrews

683e751c957d8b209cc393ff603bea937f5565b0Mark AndrewsminExpForm :: Min M_FORMULA ModalSign

683e751c957d8b209cc393ff603bea937f5565b0Mark AndrewsminExpForm ga s form =

683e751c957d8b209cc393ff603bea937f5565b0Mark Andrews let newGa = addAssocs ga s

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson ops = formulaIds s

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews preds = allPredIds s

a60f32928e486c147fa66d74ba02eda74a5d1d42Mark Andrews res = resolveFormula newGa ops preds

a60f32928e486c147fa66d74ba02eda74a5d1d42Mark Andrews minMod md ps = case md of

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews Simple_mod i -> minMod (Term_mod (Mixfix_token i)) ps

a60f32928e486c147fa66d74ba02eda74a5d1d42Mark Andrews Term_mod t -> let

a60f32928e486c147fa66d74ba02eda74a5d1d42Mark Andrews r = do

a60f32928e486c147fa66d74ba02eda74a5d1d42Mark Andrews t1 <- resolveMixfix newGa (allOpIds s) preds t

a60f32928e486c147fa66d74ba02eda74a5d1d42Mark Andrews ts <- minExpTerm minExpForm ga s t1

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews t2 <- is_unambiguous t ts ps

a60f32928e486c147fa66d74ba02eda74a5d1d42Mark Andrews let srt = term_sort t2

a60f32928e486c147fa66d74ba02eda74a5d1d42Mark Andrews trm = Term_mod t2

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews if Set.member srt $ termModies $ extendedInfo s

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews then return trm

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews else Result [mkDiag Error

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews ("unknown term modality sort '"

a60f32928e486c147fa66d74ba02eda74a5d1d42Mark Andrews ++ showId srt "' for term") t ]

a26e1cacef2047b1048febd5e8d756060b4bddb1Evan Hunt $ Just trm

a60f32928e486c147fa66d74ba02eda74a5d1d42Mark Andrews in case t of

a60f32928e486c147fa66d74ba02eda74a5d1d42Mark Andrews Mixfix_token tm ->

a60f32928e486c147fa66d74ba02eda74a5d1d42Mark Andrews if Set.member tm $ modies $ extendedInfo s

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews then return $ Simple_mod tm

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson else case maybeResult r of

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson Nothing -> Result

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson [mkDiag Error "unknown modality" tm]

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson $ Just $ Simple_mod tm

a26e1cacef2047b1048febd5e8d756060b4bddb1Evan Hunt _ -> r

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson _ -> r

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson in case form of

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson Box m f ps ->

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson do nm <- minMod m ps

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson f1 <- res f

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson f2 <- minExpFORMULA minExpForm ga s f1

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews return $ Box nm f2 ps

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews Diamond m f ps ->

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews do nm <- minMod m ps

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews f1 <- res f

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews f2 <- minExpFORMULA minExpForm ga s f1

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews return $ Diamond nm f2 ps

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrewsana_M_SIG_ITEM :: Ana M_SIG_ITEM M_FORMULA ModalSign

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrewsana_M_SIG_ITEM ga mi =

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews case mi of

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews Rigid_op_items r al ps ->

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews do ul <- mapM (ana_OP_ITEM ga) al

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews case r of

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews Rigid -> mapM_ ( \ aoi -> case item aoi of

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews Op_decl ops ty _ _ ->

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews mapM_ (updateExtInfo . addRigidOp (toOpType ty)) ops

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson Op_defn i par _ _ ->

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews updateExtInfo $ addRigidOp (toOpType $ headToType par)

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews i ) ul

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson _ -> return ()

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafsson return $ Rigid_op_items r ul ps

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafsson Rigid_pred_items r al ps ->

8f9755413f8814bbabbad40c850a81be52e05623Mark Andrews do ul <- mapM (ana_PRED_ITEM ga) al

8f9755413f8814bbabbad40c850a81be52e05623Mark Andrews case r of

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafsson Rigid -> mapM_ ( \ aoi -> case item aoi of

a60f32928e486c147fa66d74ba02eda74a5d1d42Mark Andrews Pred_decl ops ty _ ->

8f9755413f8814bbabbad40c850a81be52e05623Mark Andrews mapM_ (updateExtInfo . addRigidPred (toPredType ty)) ops

7964553eb43ab5146475841540c1c0d977e08b30Mark Andrews Pred_defn i (Pred_head args _) _ _ ->

a26e1cacef2047b1048febd5e8d756060b4bddb1Evan Hunt updateExtInfo $ addRigidPred

7964553eb43ab5146475841540c1c0d977e08b30Mark Andrews (PredType $ sortsOfArgs args) i ) ul

7964553eb43ab5146475841540c1c0d977e08b30Mark Andrews _ -> return ()

7964553eb43ab5146475841540c1c0d977e08b30Mark Andrews return $ Rigid_pred_items r ul ps

7964553eb43ab5146475841540c1c0d977e08b30Mark Andrews

7964553eb43ab5146475841540c1c0d977e08b30Mark AndrewsaddRigidOp :: OpType -> Id -> ModalSign -> Result ModalSign

7964553eb43ab5146475841540c1c0d977e08b30Mark AndrewsaddRigidOp ty i m = return

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafsson m { rigidOps = addTo i ty { opKind = Partial } $ rigidOps m }

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafsson

b043b56271060295bd32f61e7b7221dd40fb60dcMark AndrewsaddRigidPred :: PredType -> Id -> ModalSign -> Result ModalSign

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas GustafssonaddRigidPred ty i m = return

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafsson m { rigidPreds = addTo i ty $ rigidPreds m }

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafsson

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafssonana_M_BASIC_ITEM :: Ana M_BASIC_ITEM M_FORMULA ModalSign

d49d75f5073294d798aa500728116309398bb535Andreas Gustafssonana_M_BASIC_ITEM _ bi = do

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews e <- get

a26e1cacef2047b1048febd5e8d756060b4bddb1Evan Hunt case bi of

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson Simple_mod_decl al fs ps -> do

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson mapM_ ((updateExtInfo . addModId) . item) al

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson newFs <- mapAnM (resultToState (ana_M_FORMULA False)) fs

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews return $ Simple_mod_decl al newFs ps

a26e1cacef2047b1048febd5e8d756060b4bddb1Evan Hunt Term_mod_decl al fs ps -> do

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews mapM_ ((updateExtInfo . addModSort e) . item) al

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson newFs <- mapAnM (resultToState (ana_M_FORMULA True)) fs

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews return $ Term_mod_decl al newFs ps

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas GustafssonaddModId :: SIMPLE_ID -> ModalSign -> Result ModalSign

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas GustafssonaddModId i m =

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafsson let ms = modies m in

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafsson if Set.member i ms then

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafsson Result [mkDiag Hint "repeated modality" i] $ Just m

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafsson else return m { modies = Set.insert i ms }

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafsson

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas GustafssonaddModSort :: Sign M_FORMULA ModalSign -> SORT -> ModalSign -> Result ModalSign

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas GustafssonaddModSort e i m =

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafsson let ms = termModies m

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafsson ds = hasSort e i

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson in if Set.member i ms || not (null ds) then

6e8a02d5d3a845ca1768e92c88bdc0a4da47f95bAndreas Gustafsson Result (mkDiag Hint "repeated term modality" i : ds) $ Just m

6e8a02d5d3a845ca1768e92c88bdc0a4da47f95bAndreas Gustafsson else return m { termModies = Set.insert i ms }

6e8a02d5d3a845ca1768e92c88bdc0a4da47f95bAndreas Gustafsson

6e8a02d5d3a845ca1768e92c88bdc0a4da47f95bAndreas Gustafssonmap_M_FORMULA :: MapSen M_FORMULA ModalSign ()

6e8a02d5d3a845ca1768e92c88bdc0a4da47f95bAndreas Gustafssonmap_M_FORMULA mor frm =

6e8a02d5d3a845ca1768e92c88bdc0a4da47f95bAndreas Gustafsson let mapMod m = case m of

52f16aeb304bc13f6957e3ecf24c8c5b69991558Andreas Gustafsson Simple_mod _ -> return m

7d97663b2ca5b7b057276fc9d239025da80e4756Mark Andrews Term_mod t -> do newT <- mapTerm map_M_FORMULA mor t

7d97663b2ca5b7b057276fc9d239025da80e4756Mark Andrews return $ Term_mod newT

6e8a02d5d3a845ca1768e92c88bdc0a4da47f95bAndreas Gustafsson in case frm of

534253444e569bf039fb6e5fc31a5e8c2e8305c0Mark Andrews Box m f ps -> do

52f16aeb304bc13f6957e3ecf24c8c5b69991558Andreas Gustafsson newF <- mapSen map_M_FORMULA mor f

8a86c12ec245eb3838f48ffbc5a01fb9b7666a60Evan Hunt newM <- mapMod m

7c87a8bf7bc525f9b3ce80e7c12928a226e37d2bMark Andrews return $ Box newM newF ps

05398561e0221fe1fef1457627a50c60bddbb022Mark Andrews Diamond m f ps -> do

8a86c12ec245eb3838f48ffbc5a01fb9b7666a60Evan Hunt newF <- mapSen map_M_FORMULA mor f

a26e1cacef2047b1048febd5e8d756060b4bddb1Evan Hunt newM <- mapMod m

a26e1cacef2047b1048febd5e8d756060b4bddb1Evan Hunt return $ Diamond newM newF ps

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson

2e286ac71f3621c11a3409f35a859488026b5fb5Mark Andrewsana_M_FORMULA :: Bool -> FORMULA M_FORMULA -> Result (FORMULA M_FORMULA)

61d7ab455fe6c2c1be112e7f48a768b9db1f65bbMark Andrewsana_M_FORMULA b (Conjunction phis pos) = do

61d7ab455fe6c2c1be112e7f48a768b9db1f65bbMark Andrews phis' <- mapM (ana_M_FORMULA b) phis

61d7ab455fe6c2c1be112e7f48a768b9db1f65bbMark Andrews return (Conjunction phis' pos)

61d7ab455fe6c2c1be112e7f48a768b9db1f65bbMark Andrewsana_M_FORMULA b (Disjunction phis pos) = do

61d7ab455fe6c2c1be112e7f48a768b9db1f65bbMark Andrews phis' <- mapM (ana_M_FORMULA b) phis

61d7ab455fe6c2c1be112e7f48a768b9db1f65bbMark Andrews return (Disjunction phis' pos)

2e286ac71f3621c11a3409f35a859488026b5fb5Mark Andrewsana_M_FORMULA b (Implication phi1 phi2 b1 pos) = do

c85ffa76df4b94e0c44b2924f7a7f2e875a1ea86Mark Andrews phi1' <- ana_M_FORMULA b phi1

c85ffa76df4b94e0c44b2924f7a7f2e875a1ea86Mark Andrews phi2' <- ana_M_FORMULA b phi2

c85ffa76df4b94e0c44b2924f7a7f2e875a1ea86Mark Andrews return (Implication phi1' phi2' b1 pos)

c85ffa76df4b94e0c44b2924f7a7f2e875a1ea86Mark Andrewsana_M_FORMULA b (Equivalence phi1 phi2 pos) = do

c85ffa76df4b94e0c44b2924f7a7f2e875a1ea86Mark Andrews phi1' <- ana_M_FORMULA b phi1

c85ffa76df4b94e0c44b2924f7a7f2e875a1ea86Mark Andrews phi2' <- ana_M_FORMULA b phi2

c85ffa76df4b94e0c44b2924f7a7f2e875a1ea86Mark Andrews return (Equivalence phi1' phi2' pos)

c85ffa76df4b94e0c44b2924f7a7f2e875a1ea86Mark Andrewsana_M_FORMULA b (Negation phi pos) = do

c85ffa76df4b94e0c44b2924f7a7f2e875a1ea86Mark Andrews phi' <- ana_M_FORMULA b phi

c85ffa76df4b94e0c44b2924f7a7f2e875a1ea86Mark Andrews return (Negation phi' pos)

c85ffa76df4b94e0c44b2924f7a7f2e875a1ea86Mark Andrewsana_M_FORMULA _ phi@(True_atom _) = return phi

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrewsana_M_FORMULA _ phi@(False_atom _) = return phi

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrewsana_M_FORMULA _ (Mixfix_formula (Mixfix_token ident)) =

3d2ce18535b3d2d828bd40aec7f4686519f305feMark Andrews return (Predication (Qual_pred_name (mkId [ident])

3d2ce18535b3d2d828bd40aec7f4686519f305feMark Andrews (Pred_type [] []) [])

3d2ce18535b3d2d828bd40aec7f4686519f305feMark Andrews [] [])

3d2ce18535b3d2d828bd40aec7f4686519f305feMark Andrewsana_M_FORMULA b (ExtFORMULA (Box m phi pos)) = do

3d2ce18535b3d2d828bd40aec7f4686519f305feMark Andrews phi' <- ana_M_FORMULA b phi

3d2ce18535b3d2d828bd40aec7f4686519f305feMark Andrews return(ExtFORMULA (Box m phi' pos))

3d2ce18535b3d2d828bd40aec7f4686519f305feMark Andrewsana_M_FORMULA b (ExtFORMULA (Diamond m phi pos)) = do

3d2ce18535b3d2d828bd40aec7f4686519f305feMark Andrews phi' <- ana_M_FORMULA b phi

3d2ce18535b3d2d828bd40aec7f4686519f305feMark Andrews return(ExtFORMULA (Diamond m phi' pos))

3d2ce18535b3d2d828bd40aec7f4686519f305feMark Andrewsana_M_FORMULA b phi@(Quantification _ _ phi1 pos) =

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrews if b then ana_M_FORMULA b phi1

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrews else anaError phi pos

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrewsana_M_FORMULA _ phi@(Predication _ _ pos) =

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrews return phi -- should lookup predicate!

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrewsana_M_FORMULA _ phi@(Definedness _ pos) =

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrews anaError phi pos

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrewsana_M_FORMULA _ phi@(Existl_equation _ _ pos) =

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrews anaError phi pos

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrewsana_M_FORMULA _ phi@(Strong_equation _ _ pos) =

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrews anaError phi pos

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrewsana_M_FORMULA _ phi@(Membership _ _ pos) =

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrews anaError phi pos

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrewsana_M_FORMULA _ phi@(Mixfix_formula _) =

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrews return phi -- should do mixfix analysis and lookup predicate!

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrews -- anaError phi [nullPos]

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrewsana_M_FORMULA _ phi@(Unparsed_formula _ pos) =

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrews anaError phi pos

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrewsana_M_FORMULA _ phi@(Sort_gen_ax _ _) =

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrews anaError phi [nullPos]

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrews

d49d75f5073294d798aa500728116309398bb535Andreas GustafssonanaError :: a -> [Pos] -> Result a

d49d75f5073294d798aa500728116309398bb535Andreas GustafssonanaError phi pos =

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson plain_error phi

1090574e9153ad41c403f812d9b6cef0334e828eMark Andrews "Modality declarations may only contain propositional axioms"

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson (headPos pos)