hylotab-1.2.0: src/Hylotab.hs
module Hylotab where
import Data.List ( nub, intersect, (\\) )
import Form ( Form(..), NomSymbol(..), PropSymbol(..), RelSymbol(..), Rel, parse )
import Control.Monad(when)
type Index = Int
type Domain = [NomSymbol]
{- Generic Satisfiability Checking -}
-- Distinguish between two modes of satisfiability checking:
data Mode = Extend -- for extending with a new nominal at each
-- encounter with a diamond
| Try -- for trial and error extension, including
-- checking existing nominals
-- If psi defines a frame property, then any model M satisfying (A psi)
-- will be in the frame class with that property. For suppose that
-- M does not have the frame property. Then there is a world w with
-- M , w |/= psi, hence M |/= A psi. Thus, we can
-- build an engine for the frame class of psi by loading the proof
-- engine with (A psi) as a universal constraint. This leads to the
-- following generic satisfiability checker (the first argument gives
-- the mode of satisfiability checking, the second argument lists the
-- formulas defining the frame class under consideration):
data SatFlag = SAT Tableau | UNSAT
genSat :: Bool -> Mode -> [Form] -> Form -> IO SatFlag
genSat verbose Extend props form =
do res <- expand verbose (initTab form props)
case res of
OPEN nodes -> return $ SAT nodes
CLOSED -> return UNSAT
genSat verbose Try props form =
do res <- cautiousExpand verbose (initTab form props)
case res of
OPEN nodes -> return $ SAT nodes
CLOSED -> return UNSAT
{- Theorem Proving -}
-- The function initTab creates an initial tableau for a
-- formula. The initial tableau for phi is just one node, with list of
-- pending formulas [@ m phi], where m is a fresh nominal. We assume
-- that no nominals of the form (N i) appear in the formula. The
-- node index is set to the index of the first fresh constant nominal,
-- i.e., 1.
initTab :: Form -> [Form] -> Tableau
initTab form props =
[Nd {idx = 1 + newIdx,
dom = dom',
neqs = [], accs = [], ufs = [],
boxes = [], cboxes = [], pos = [],
neg = [], forms= forms'
}
]
where noms = nomsInForms (form:props)
newIdx = case noms of
[] -> 0
_ -> 1 + maximum [ n | (N n) <- noms]
newNom = N newIdx
dom' = newNom : nomsInForms (form:props)
forms' = [At newNom form] ++
case props of
[] -> []
[prop] -> [At newNom (A prop)]
_ -> [At newNom (A (Conj props))]
{- Tableau Nodes and Tableaux -}
-- A node of a tableau consists of
data Node = Nd { idx :: Index, -- a tableau index (needed to generate fresh tableau parameters)
dom :: Domain, -- a domain (all nominals occurring at the node)
neqs :: [(NomSymbol,NomSymbol)], -- a list of n != m constraints on the node
accs :: [(NomSymbol,Rel,NomSymbol)], -- a list of n<Ri>m accessibilities on the node
ufs :: [Form], -- the A formulas that have been applied to all nominals in the domain of the node
boxes :: [(NomSymbol,Rel,Form)], -- the (@n [i] phi) formulas of the node that have been combined
-- with all the (n<i>m) accessibilities on the node
-- (the boxed constraints of the node)
cboxes :: [(NomSymbol,Rel,Form)], -- the (@n [-i] phi) formulas of the node that have
-- been combined with all the (m<i>n) accessibilities on the node
-- (the converse boxed constraints of the node)
pos :: [(NomSymbol,PropSymbol)], -- the positive atom attributions (@ n p_i) on the node
neg :: [(NomSymbol,PropSymbol)], -- the negative atom attributions (@ n - p_i) on the node
forms :: [Form] -- pending formulas yet to be treated by the proof engine
}
deriving (Eq)
instance Show Node where
show nd
= unlines ["Node:",
"index: " ++ show (idx nd),
"domain: " ++ show (dom nd),
"neqs: " ++ show (neqs nd),
"accs: " ++ show (accs nd),
"ufs: " ++ show (ufs nd),
"boxes: " ++ show (boxes nd),
"cboxes: " ++ show (cboxes nd),
"pos: " ++ show (pos nd),
"neg: " ++ show (neg nd),
"formulas: " ++ show (forms nd)]
type Tableau = [Node]
-- collect the constant nominals and the free occurrences of
-- variable nominals from a formula or a formula list.
nomsInForm :: Form -> [NomSymbol]
nomsInForm (Nom nom) = [nom]
nomsInForm (Neg f) = nomsInForm f
nomsInForm (Conj fs) = nomsInForms fs
nomsInForm (Disj fs) = nomsInForms fs
nomsInForm (Impl f1 f2) = nomsInForms [f1,f2]
nomsInForm (A f) = nomsInForm f
nomsInForm (E f) = nomsInForm f
nomsInForm (Box _ f) = nomsInForm f
nomsInForm (Dia _ f) = nomsInForm f
nomsInForm (At nom f) = add nom (nomsInForm f)
nomsInForm (Down x f) = filter (/= x) (nomsInForm f)
nomsInForm _ = []
nomsInForms :: [Form] -> [NomSymbol]
nomsInForms = nub . concatMap nomsInForm
type Subst = (NomSymbol,NomSymbol)
-- Application of a substitution to a nominal:
appNom :: Subst -> NomSymbol -> NomSymbol
appNom (n,m) nom = if n == nom then m else nom
-- Application of a substitution to a domain. Note that the substitution
-- may identify individuals, so after the substitutition we have to clean
-- up the list with nub to remove possible duplicates.
appDomain :: Subst -> Domain -> Domain
appDomain = map . appNom
appNNs :: Subst -> [(NomSymbol,NomSymbol)] -> [(NomSymbol,NomSymbol)]
appNNs b = map (\ (n,m) -> (appNom b n, appNom b m))
appNRNs :: Subst -> [(NomSymbol,Rel,NomSymbol)] -> [(NomSymbol,Rel,NomSymbol)]
appNRNs b = map (\ (n,r,m) -> (appNom b n, r, appNom b m))
appNPs :: Subst -> [(NomSymbol,PropSymbol)] -> [(NomSymbol,PropSymbol)]
appNPs b = map (\ (n,name) -> (appNom b n, name))
-- Application of a substitution to a formula or a formula list.
-- Note that substitutions only affect the _free_
-- variables of a formula
appF :: Subst -> Form -> Form
appF _ Top = Top
appF _ Bot = Bot
appF _ (Prop p) = Prop p
appF b (Nom nom) = Nom (appNom b nom)
appF b (Neg f) = Neg (appF b f)
appF b (Conj fs) = Conj (appFs b fs)
appF b (Disj fs) = Disj (appFs b fs)
appF b (Impl f1 f2) = Impl (appF b f1) (appF b f2)
appF b (A f) = A (appF b f)
appF b (E f) = E (appF b f)
appF b (Box r f) = Box r (appF b f)
appF b (Dia r f) = Dia r (appF b f)
appF b (At n f) = At (appNom b n) (appF b f)
appF b (Down n f) = Down (appNom b n) (appF b f)
appFs :: Subst -> [Form] -> [Form]
appFs = map . appF
appNRFs :: Subst -> [(NomSymbol,Rel,Form)] -> [(NomSymbol,Rel,Form)]
appNRFs b = map (\ (n,r,f) -> (appNom b n, r, appF b f))
{- Formulas compensating lack of pattern matching -}
isAlpha, isBeta :: Form -> Bool
isAlpha (Conj _) = True
isAlpha (Neg (Disj _)) = True
isAlpha (Neg (Impl _ _)) = True
isAlpha _ = False
isBeta (Disj _) = True
isBeta (Impl _ _) = True
isBeta (Neg (Conj _)) = True
isBeta _ = False
isA, isE :: Form -> Bool
isA (A _) = True
isA (Neg (E _)) = True
isA _ = False
isE (E _) = True
isE (Neg (A _)) = True
isE _ = False
isBox, isDiamond :: Form -> Bool
isBox (Box _ _) = True
isBox (Neg (Dia _ _)) = True
isBox _ = False
isDiamond (Dia _ _) = True
isDiamond (Neg (Box _ _)) = True
isDiamond _ = False
isDown, isLabel :: Form -> Bool
isDown (Down _ _ ) = True
isDown (Neg (Down _ _ )) = True
isDown _ = False
isLabel (At _ _) = True
isLabel (Neg (At _ _)) = True
isLabel _ = False
isTrue,isFalse,isPlit, isNlit :: Form -> Bool
isTrue Top = True
isTrue _ = False
isFalse Bot = True
isFalse _ = False
isPlit (Prop _) = True
isPlit _ = False
isNlit (Neg (Prop _)) = True
isNlit _ = False
isNom, isNgNom, isAcc, isDneg :: Form -> Bool
isNom (Nom _) = True
isNom _ = False
isNgNom (Neg (Nom _)) = True
isNgNom _ = False
isAcc (Dia _ (Nom _)) = True
isAcc (Neg (Box _ (Neg (Nom _)))) = True
isAcc _ = False
isDneg (Neg (Neg _)) = True
isDneg _ = False
isInvRel :: Form -> Bool
isInvRel (Box (RelSymbol _) _) = False
isInvRel (Dia (RelSymbol _) _) = False
isInvRel (Neg (Box (RelSymbol _) _)) = False
isInvRel (Neg (Dia (RelSymbol _) _)) = False
isInvRel (Box (InvRelSymbol _) _) = True
isInvRel (Dia (InvRelSymbol _) _) = True
isInvRel (Neg (Box (InvRelSymbol _) _)) = True
isInvRel (Neg (Dia (InvRelSymbol _) _)) = True
isInvRel f = error $ "error isInvRel: " ++ show f
-- Function for converting a literal (a propositional atom or a negation
-- of a propositional atom) at a nominal n to a pair consisting of the
-- n and the name of the atom.
nf2np :: NomSymbol -> Form -> (NomSymbol,PropSymbol)
nf2np nom (Prop name) = (nom,name)
nf2np nom (Neg (Prop name)) = (nom,name)
nf2np _ _ = error "error nf2np"
-- Function for converting a nominal m or negated nominal !m, at a
-- nominal n, to the pair (n,m).
nf2nn :: NomSymbol -> Form -> (NomSymbol,NomSymbol)
nf2nn n (Nom m) = (n,m)
nf2nn n (Neg (Nom m)) = (n,m)
nf2nn _ _ = error "error nf2nn"
-- Function for getting the nominal out of a nominal formula, a negated
-- nominal formula, or an access formula
getNom :: Form -> NomSymbol
getNom (Nom nom) = nom
getNom (Neg (Nom nom)) = nom
getNom (Dia _ (Nom nom)) = nom
getNom (Neg (Box _ (Neg (Nom nom)))) = nom
getNom _ = error "error getNom"
-- Function for getting the relation and the target nominal out of a
-- box or diamond formula:
getRel :: Form -> Rel
getRel (Neg f) = getRel f
getRel (Dia (RelSymbol rel) _) = rel
getRel (Dia (InvRelSymbol rel) _) = rel
getRel (Box (RelSymbol rel) _) = rel
getRel (Box (InvRelSymbol rel) _) = rel
getRel _ = error "error getRel"
-- The components of a (non-literal) formula are given by:
components :: Form -> [Form]
components (Conj fs) = fs
components (Disj fs) = fs
components (Impl f1 f2) = [Neg f1,f2]
components (Neg (Conj fs)) = map Neg fs
components (Neg (Disj fs)) = map Neg fs
components (Neg (Impl f1 f2)) = [f1,Neg f2]
components (Neg (Neg f)) = [f]
components (A f) = [f]
components (Neg (A f)) = [Neg f]
components (E f) = [f]
components (Neg (E f)) = [Neg f]
components (Box _ f) = [f]
components (Neg (Box _ f)) = [Neg f]
components (Dia _ f) = [f]
components (Neg (Dia _ f)) = [Neg f]
components (Down _ f) = [f]
components (Neg (Down _ f)) = [Neg f]
components (At _ f) = [f]
components (Neg (At _ f)) = [Neg f]
components _ = error "error components"
-- Located components of a (non-literal) formula:
lcomponents :: NomSymbol -> Form -> [Form]
lcomponents nom f = [At nom f' | f' <- components f ]
-- For label formulas, the following function returns the label:
getLabel :: Form -> NomSymbol
getLabel (At nom _) = nom
getLabel (Neg (At nom _)) = nom
getLabel _ = error "error getLabel"
-- For binder formulas, the following function returns the binder:
binder :: Form -> Int
binder (Down (X x) _) = x
binder (Neg (Down (X x) _)) = x
binder _ = error "error binder"
-- Check a list of formulas for nominal contradiction.
checkNom :: [Form] -> Bool
checkNom fs = null [ m | (At n (Neg (Nom m))) <- fs, m == n ]
-- Checking a node for closure, with closure indicated by return of []
check :: Node -> [Node]
check node =
if checkNN (neqs node)
&& checkPN (pos node) (neg node)
&& checkNom (forms node)
then [node] else []
where checkNN = all (\(m,n) -> m /= n)
checkPN poss negs = intersect poss negs == []
-- Sometimes we just have to check the final component of a node:
checkNdNom :: Node -> [Node]
checkNdNom node = if checkNom (forms node) then [node] else []
{- Tableau Expansion -}
step :: Node -> Tableau
-- Applying an expansion step to a node N yields a tableau, i.e., a list
-- of nodes. If the expansion step results in closure of N, we return
-- []. Otherwise we return a non-empty list of open tableau nodes.
-- If the function is called for a node N with an empty pending formula
-- list, there is nothing left to do, so we return [N].
step node | null (forms node) = check node
-- If the list of pending formulas starts with a Boolean constant, then
-- remove it if it is the constant True, otherwise close the node:
step node
| isTrue f = [node{forms=fs}]
| isFalse f = []
-- The list of pending formulas starts with a propositional literal:
-- check for closure; if the node does not close, then add the literal to
-- the appropriate list.
| isPlit f = let
ni = nf2np nom f
pos' = add ni (pos node)
in
if ni `elem` neg node then []
else [node{forms=fs, pos=pos'}]
| isNlit f = let
ni = nf2np nom f
neg' = add ni (neg node)
in
if ni `elem` pos node then []
else [node{forms=fs, neg=neg'}]
-- The list of pending formulas starts with a nominal. In this case we
-- perform a substitution and check for closure. Note the following:
-- * Applying a substitution to a list of access relations may result
-- in a _change_ in the access relations, and thus in a violation of
-- a universal constraint, thus destroying the invariant that the universal
-- constraints hold for all nominals present at the node. To restore
-- that invariant, we have to take care that the universal constraints
-- get (re-)applied to the new nominal that fuses two old ones.
-- * Applying a
-- substitution to a list of access relations may result in new access
-- relations, thus destroying the invariant that the box and converse box
-- constraints of the node have been applied for all access relations of
-- the node. To restore that invariant, we have to take care that all box
-- and converse box constraints get applied to the new access relations.
-- * Applying a substitution to a list of box constraints may result
-- in new box constraints, thus destroying the invariant that the box
-- constraints of the node have been applied for all access relations of
-- the node. To restore that invariant, we have to apply all new box
-- constraints to all access relations of the node.
-- * Applying a substitution to a list of converse box constraints may result
-- in new converse box constraints, thus destroying the invariant that
-- the converse box constraints of the node have been applied for all
-- access relations of the node. To restore that invariant, we have to
-- apply all new converse box constraints to all access relations of the
-- node.
| isNom f =
if getNom f == nom
then [node{forms=fs}]
else
let
k_ = getNom f
m = min k_ nom
n = max k_ nom
dom' = nub $ appDomain (n,m) (dom node)
neqs' = nub $ appNNs (n,m) (neqs node)
accs' = nub $ appNRNs (n,m) (accs node)
ufs' = nub $ appFs (n,m) (ufs node)
boxes' = nub $ appNRFs (n,m) (boxes node)
newboxes = boxes' \\ boxes node
cboxes' = nub $ appNRFs (n,m) (cboxes node)
newcboxes = cboxes' \\ cboxes node
pos' = nub $ appNPs (n,m) (pos node)
neg' = nub $ appNPs (n,m) (neg node)
forms' = nub $ appFs (n,m) (forms node)
newaccs = accs' \\ accs node
us = [ At m g | g <- ufs' ]
bs1 = [ At l g | (k,r,l) <- newaccs,
(k',r',g) <- boxes',
k == k', r == r' ]
bs2 = [ At l g | (k,r,l) <- accs',
(k',r',g) <- newboxes,
k == k', r == r' ]
cs1 = [ At k g | (k,r,l) <- newaccs,
(l',r',g) <- cboxes',
l == l', r == r' ]
cs2 = [ At k g | (k,r,l) <- accs',
(l',r',g) <- newcboxes,
l == l', r == r' ]
newforms = nub $ forms' ++ us ++ bs1 ++ bs2 ++ cs1 ++ cs2
in
check node{dom = dom',
neqs = neqs',
accs = accs',
ufs = ufs',
boxes = boxes',
cboxes = cboxes',
pos = pos',
neg = neg',
forms = newforms}
-- The list of pending formulas starts with a negated nominal: check for
-- closure. If the node does not close, add a new inequality (m != n)
-- to the inequality list of the node.
| isNgNom f =
if getNom f == nom
then []
else
let
k = getNom f
m = min k nom
n = max k nom
neqs' = add (m,n) (neqs node)
in
[node{neqs = neqs', forms = fs}]
-- The list of pending formulas starts with an access formula
| isAcc f && not (isInvRel f)
=
let
(r,n) = (getRel f, getNom f)
accs' = add (nom,r,n) (accs node)
dom' = add n (dom node)
fs' = if (nom,r,n) `elem` accs node -- check is the access relation is already in the node
then fs
else nub $ fs ++ us ++ bs ++ cs
us = [ At n g | g <- ufs node ] -- add universal constraints
bs = [ At n g | (m,s,g) <- boxes node,
m == nom, s == r ] -- add box constaints
cs = [ At nom g | (m,s,g) <- cboxes node,
m == n, s == r ] -- add inverse box constraints
in
checkNdNom node{dom = dom',
accs = accs',
forms = fs'
}
| isAcc f && isInvRel f
=
let
(r,n) = (getRel f, getNom f)
accs' = add (n,r,nom) (accs node)
dom' = add n (dom node)
fs' = if (n,r,nom) `elem` accs node
then fs
else nub $ fs ++ us ++ bs ++ cs
us = [ At n g | g <- ufs node ]
bs = [ At nom g | (m,s,g) <- boxes node,
m == n, s == r ]
cs = [ At n g | (m,s,g) <- cboxes node,
m == nom, s == r ]
in
checkNdNom node{dom = dom',
accs = accs',
forms = fs'
}
-- The list of pending formulas starts with a double negation: apply the
-- double negation rule.
| isDneg f
= let
[g] = lcomponents nom f
fs' = add g fs
in
[node{forms=fs'}]
-- The list of pending formulas starts with an alpha formula:
-- add the components alpha_i to the node.
| isAlpha f =
let
fs' = nub $ lcomponents nom f ++ fs
in
[node{forms=fs'}]
-- The list of pending formulas starts with a beta formula:
-- split the node and add a component beta_i to each new branch.
| isBeta f = [ node{forms=(f':fs)} | f' <- lcomponents nom f ]
-- The list of pending formulas starts with an A formula (@ k phi).
-- Add { @ m phi' | m in D } where D is
-- the domain of the node, to the list of pending formulas, and store
-- phi' as a universal constraint.
| isA f = let
newfs = [ At n g | n <- dom node,
g <- components f ]
fs' = nub $ fs ++ newfs
[f'] = components f
ufs' = nub (f':ufs node)
in
checkNdNom node{ufs = ufs',
forms = fs'}
-- The list of pending formulas starts with an E formula (@ k phi).
-- Take a fresh nominal n, add it to the domain of the node,
-- add (@ n phi') and { @ n psi | psi in U } to the list
-- of pending formulas.
| isE f = let
n = N (idx node)
dom' = add n (dom node)
ls = lcomponents n f
us = [ At n g | g <- ufs node ]
fs' = nub $ fs ++ ls ++ us
in
[node{idx=(succ $ idx node), dom=dom', forms=fs'}]
-- The list of pending formulas starts with a [i] formula (@k phi).
-- Add the list [@ m phi' | k<i>m in A ],
-- where A is the list of access formulas of the node, to the list of
-- pending formulas, and store the [i] formula as a box
-- constraint. Actually, for convenience, we store (k,i,phi').
| isBox f && not (isInvRel f)
= let
r = getRel f
newfs = [ At n g | (m,s,n) <- accs node,
g <- components f,
m == nom, s == r ]
fs' = nub $ fs ++ newfs
boxes' = nub $
[(nom,r,g) | g <- components f] ++ boxes node
in
checkNdNom node{boxes=boxes',forms=fs'}
-- The list of pending formulas starts with a [-i] formula
-- (@k phi). Add the list [@ m phi' | m<i>k in A]
-- where A is the list of access formulas of the node, to the list of
-- pending formulas, and store the [-i] formula as a converse box
-- constraint. Actually, for convenience we store (k,i,phi').
| isBox f && isInvRel f
= let
r = getRel f
newfs = [ At n g | (n,s,m) <- accs node,
g <- components f,
m == nom, s == r ]
fs' = nub $ fs ++ newfs
cboxes' = nub $
[(nom,r,g) | g <- components f] ++ cboxes node
in
checkNdNom node{cboxes=cboxes', forms=fs'}
-- The list of pending formulas starts with a diamond formula: use the
-- node index i to generate a fresh nominal constant n_i, increment
-- the node index, add (k<j>n_i) to the access list of the node, and put
-- (@ n_i phi'), where phi' is the component of the diamond
-- formula, on the list of pending formulas. Also, generate appropriate
-- formulas for n_i from the universal constraints and from the
-- box constraints on k, and append them to the list of pending formulas.
| isDiamond f && not (isInvRel f)
=
let
n = N (idx node)
idx' = succ $ idx node
r = getRel f
accs' = (nom,r,n):(accs node)
dom' = add n (dom node)
ls = lcomponents n f
us = [ At n g | g <- ufs node ]
bs = [ At n g | (m,s,g) <- boxes node,
m == nom, s == r ]
fs' = nub $ fs ++ ls ++ us ++ bs
in
[node{idx=idx', dom=dom', accs=accs', forms=fs'}]
-- The list of pending formulas starts with a inverse diamond
-- formula: use the node index i to generate a fresh nominal constant
-- n_i, increment the node index, add (n_i<j>k) to the access list of
-- the node, generate the appropriate formulas for n_i from the converse
-- box constraints of the node, and append them, together with the
-- component of the <-> formula, to the list of pending formulas.
| isDiamond f && isInvRel f
=
let
n = N (idx node)
idx' = succ $ idx node
r = getRel f
accs' = (n,r,nom):(accs node)
dom' = add n (dom node)
ls = lcomponents n f
us = [ At n g | g <- ufs node ]
cs = [ At n g | (m,s,g) <- cboxes node,
m == nom, s == r ]
fs' = nub $ fs ++ ls ++ us ++ cs
in
[node{idx = idx', dom=dom', accs=accs', forms=fs'}]
-- The list of pending formulas starts with an @ formula (@k @n phi)
-- (or (@ k - @ n phi)): add (@ n phi) (or (@ n - phi)) to the
-- list of pending formulas.
| isLabel f
= let
fs' = add f' fs
n = getLabel f
[f'] = lcomponents n f
in
[node{forms=fs'}]
-- The list of pending formulas starts with a down-arrow formula: add
-- its component to the list of pending formulas, after the appropriate
-- substitution.
| isDown f
= let
x = binder f
[g] = components f
f' = At nom (appF (X x,nom) g)
fs' = add f' fs
in
[node{forms=fs'}]
where (At nom f:fs) = forms node
step nd = error $ "error step: " ++ show nd
-- These are all the possible cases, so this ends the treatment of
-- a single tableau expansion step.
-- A tableau node is fully expanded (complete) if its list of pending
-- formulas is empty.
complete :: Node -> Bool
complete node | null $ forms node = True
complete _ = False
-- In general, we are not interested in generating all models for
-- a satisfiable formula: one model is enough. This allows for
-- a considerable reduction.
data OpenFlag = OPEN [Node] | CLOSED
expand :: Bool -> Tableau -> IO OpenFlag
expand verbose [] = do when verbose $ putStrLn "Closed"
return CLOSED
expand verbose (node:nodes) =
do when verbose $ putStrLn (show node)
if complete node
then return $ OPEN [node]
else do let newnodes = step node
expand verbose (nodes ++ newnodes)
{- Cautious Tableau Expansion -}
-- Tableau expansion according to the `trial and error' versions of the
-- E, Diamond and Cdia rules is useful for finding minimal
-- models. In cautious tableau expansion we reuse existing nominals, and
-- we should check carefully whether this disturbs our constraints
-- invariant. The following functions take care of this:
noAccTo, noAccFrom :: [(NomSymbol,Rel,NomSymbol)] -> NomSymbol -> Rel -> Bool
noAccTo accs_ m r = null [ (k,r,m) | (k,r',m') <- accs_, r==r', m==m' ]
noAccFrom accs_ m r = null [ (m,r,k) | (m',r',k) <- accs_, r==r', m==m' ]
-- Thus, if (noAccTo accs m r) is true at a node, where accs
-- is the list of access arrows of the node, this means that there
-- is no arrow (x <r> m) at the
-- node. This means in turn that adding a new r arrow that
-- points to m may disturb the box constraint invariant. Similarly,
-- truth of (noAccFrom accs m r) at a node, accs
-- is the list of access arrows of the node, indicates that the addition
-- of a new r-relation arrow that departs from m may violate
-- the converse box constraint invariant of the node.
--
-- We are ready now to replace the step function by the following
-- alternative:
cautiousStep :: Node -> Tableau
-- Cautious step are like ordinary steps, except for the cases where
-- the formula to be decomposed is a E, Diamond and Cdia formula.
--
-- If the function is called for a node N with an empty pending formula
-- list, again, there is nothing left to do, and we return [N].
cautiousStep node
| null $ forms node = [node]
-- If the list of pending formulas starts with an E formula, we branch
-- to all the possible ways of letting the existential obligation be
-- fulfilled by an existing nominal, and append the result of doing the
-- extension step that introduces a fresh nominal. Note that no accessibilities
-- are added, so no box or converse box constraints can be violated. Also,
-- no nominals are added, so no universal constraints can be violated.
| isE f =
[ node{forms = nub (lcomponents n f ++ fs)} | n <- dom node]
++ step node
-- If the list of pending formulas starts with a Diamond or Cdia formula,
-- we branch to all the ways of letting an existing nominal discharge
-- the existential obligation, and append the result of the
-- expansion step that introduces a fresh nominal. Now we have to
-- take measures to ensure that the invariant for the box constraints
-- gets restored, if necessary.
| isDiamond f && not (isInvRel f)
=
let r = getRel f in
[ node{accs = add (nom,r,n) (accs node),
forms= nub (lcomponents n f ++ fs ++ [ At n g | (m,s,g) <- boxes node, m == nom, s == r, noAccTo (accs node) n r ])
} | n <- dom node ]
++ step node
| isDiamond f && isInvRel f
=
let r = getRel f in
[ node{accs = add (n,r,nom) (accs node),
forms= nub (lcomponents n f ++ fs ++ [ At n g | (m,s,g) <- cboxes node, m == nom, s == r,noAccFrom (accs node) n r ])
} | n <- dom node]
++ step node
| otherwise = step node
where (At nom f:fs) = forms node
-- Cautious expansion of a tableau:
cautiousExpand :: Bool -> Tableau -> IO OpenFlag
cautiousExpand verbose [] = do when verbose $ putStrLn "Closed"
return CLOSED
cautiousExpand verbose (node:nodes) =
do when verbose $ putStrLn (show node)
if complete node
then return $ OPEN [node]
else do let newnodes = cautiousStep node
cautiousExpand verbose (nodes ++ newnodes)
{- Model Generation -}
extract :: Node -> String
extract node =
unwords $
show (reverse (dom node))
: [ show n ++ show i ++ show m | (n,i,m) <- reverse (accs node)]
++ [ show i ++ ":" ++ show p | (i,p) <- reverse (pos node) ]
++ [ show i ++ ":-" ++ show p | (i,p) <- reverse (neg node) ]
{- Frame Properties -}
-- Here is a list of pure formulas (formulas without proposition letters)
-- that define frame properties. In fact, any pure formula defines
-- a frame condition, and characterizes a class of frames.
trans, k4, intrans, refl, kt, irrefl, symm :: Form
kb, asymm, s4, kt4, s5, serial, kd, euclid, k5 :: Form
kdb, kd4, kd5, k45, kd45, kb4, ktb, antisymm :: Form
trans = parse "begin down x1 . [][]<->x1 end"
k4 = trans
intrans = parse "begin down x1 . [][][-]-x1 end"
refl = parse "begin down x1 . <>x1 end"
kt = refl
irrefl = parse "begin down x1 . []-x1 end"
symm = parse "begin down x1 . []<>x1 end"
kb = symm
asymm = parse "begin down x1 . [][]-x1 end"
s4 = parse "begin down x1 . (<>x1 & [][] <->x1) end"
kt4 = s4
s5 = parse "begin down x1 . ((<>x1) & ([]<>x1) & ([][]<->x1)) end"
serial = parse "begin <>true end"
kd = serial
euclid = parse "begin down x1 . [] down x2 . @ x1 []<>x2 end"
k5 = euclid
kdb = parse "begin (<>true & down x1 . []<->x1) end"
kd4 = parse "begin (<>true & down x1 . [][]<->x1) end"
kd5 = parse "begin (<>true & down x1 . [] down x2 . @ x1 []<>x2) end"
k45 = parse "begin down x1 . x1([][]<->1 & [] down x2 . @ x1 []<>x2) end"
kd45 = parse "begin down x1 . ((<>true) & ([][]<->x1) & ([] down x2 . @ x1 []<>x2)) end"
kb4 = parse "begin down x1 . ([]<>x1 & [][] <->x1) end"
ktb = parse "begin down x1 . (<>x1 & []<>x1) end"
antisymm = parse "begin down x1 . [] down x2 . [] (x1 -> x2) end"
add :: (Eq a) => a -> [a] -> [a]
add x xs = if x `elem` xs then xs else x:xs