Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
- data CriticalSequenceType
- data CriticalSequence m
- getCriticalSequenceMatches :: CriticalSequence m -> Maybe (m, m)
- getCriticalSequenceComatches :: CriticalSequence m -> (m, m)
- getNacMatchOfCriticalSequence :: CriticalSequence m -> Maybe m
- getNacIndexOfCriticalSequence :: CriticalSequence m -> Maybe Int
- getCriticalSequenceType :: CriticalSequence m -> CriticalSequenceType
- findTriggeringCriticalSequences :: (EpiPairs m, DPO m) => MorphismsConfig -> Production m -> Production m -> [CriticalSequence m]
- namedCriticalSequences :: (EpiPairs m, DPO m) => MorphismsConfig -> [NamedRule m] -> [NamedCriticalPairs m]
- findAllProduceUse :: (DPO m, EpiPairs m) => MorphismsConfig -> Production m -> Production m -> [CriticalSequence m]
- findAllRemoveDangling :: (EpiPairs m, DPO m) => MorphismsConfig -> Production m -> Production m -> [CriticalSequence m]
- findAllDeleteForbid :: (DPO m, EpiPairs m) => MorphismsConfig -> Production m -> Production m -> [CriticalSequence m]
- findAllDeliverDelete :: (DPO m, EpiPairs m) => MorphismsConfig -> Production m -> Production m -> [CriticalSequence m]
- findAllForbidProduce :: (DPO m, EpiPairs m) => MorphismsConfig -> Production m -> Production m -> [CriticalSequence m]
- findAllDeliverDangling :: (DPO m, EpiPairs m) => MorphismsConfig -> Production m -> Production m -> [CriticalSequence m]
- findAllProduceUseAndRemoveDangling :: (EpiPairs m, DPO m) => MorphismsConfig -> Production m -> Production m -> [CriticalSequence m]
Documentation
data CriticalSequenceType Source #
Data representing the type of a CriticalPair
ProduceUse | resp. delete-use |
RemoveDangling | resp. produce-dangling |
DeleteForbid | resp. produce-forbid |
DeliverDelete | resp. inverted delete-use |
DeliverDangling | resp. inverted produce-dangling |
ForbidProduce | resp. inverted produce-forbid |
data CriticalSequence m Source #
A Critical Sequence is defined as two matches (m1,m2) from the left side of their rules to a same graph.
This diagram shows graphs and morphisms names used in the algorithms below
p1 = production (L1,K1,R1,[N1]) (N1 from L1)
invLeft = production (R1,K1,L1,[N1]) (N1 from R1)
p2 = production (L2,K2,R2,[N2])
N1 N2 ^ ^ l r │ │n L1◀─────K1────▶R1 L2◀────K2─────▶R2 │ │ \ / │ │ m1│ k│ m1'\ /m2' │ │ ▼ ▼ ▼ ▼ ▼ P1◀─────D1───────▶G◀───────D2──────▶P2 r' l'
m2 :: from L2 to P1
h21 :: from L2 to D1
q21 (nacMatch) :: from N2 to P1
Eq m => Eq (CriticalSequence m) Source # | |
Show m => Show (CriticalSequence m) Source # | |
getCriticalSequenceMatches :: CriticalSequence m -> Maybe (m, m) Source #
Returns the matches (m1, m2)
getCriticalSequenceComatches :: CriticalSequence m -> (m, m) Source #
Returns the comatches (m1', m2')
getNacMatchOfCriticalSequence :: CriticalSequence m -> Maybe m Source #
Returns the nac match of a CriticalSequence
getNacIndexOfCriticalSequence :: CriticalSequence m -> Maybe Int Source #
Returns the nac index of a CriticalSequence
getCriticalSequenceType :: CriticalSequence m -> CriticalSequenceType Source #
Returns the type of a CriticalSequence
Finding Critical Sequences
findTriggeringCriticalSequences :: (EpiPairs m, DPO m) => MorphismsConfig -> Production m -> Production m -> [CriticalSequence m] Source #
Given two productions p1
and p2
, finds the Critical sequences in which the application of p1
enables the application of p2
namedCriticalSequences :: (EpiPairs m, DPO m) => MorphismsConfig -> [NamedRule m] -> [NamedCriticalPairs m] Source #
Returns the Critical Sequences with rule names
findAllProduceUse :: (DPO m, EpiPairs m) => MorphismsConfig -> Production m -> Production m -> [CriticalSequence m] Source #
All ProduceUse caused by the derivation of l
before r
.
Rule p1
causes a produce-use dependency with p2
if rule p1
creates something that is used by p2
.
Verify the non existence of h21: L2 -> D1 such that d1 . h21 = m2'.
findAllRemoveDangling :: (EpiPairs m, DPO m) => MorphismsConfig -> Production m -> Production m -> [CriticalSequence m] Source #
All RemoveDangling caused by the derivation of p1
before p2
.
Rule p1
causes a remove-dangling dependency with p2
if rule p1
deletes something that enables p2
.
findAllDeleteForbid :: (DPO m, EpiPairs m) => MorphismsConfig -> Production m -> Production m -> [CriticalSequence m] Source #
All DeleteForbid caused by the derivation of p1
before r
.
Rule p1
causes a delete-forbid dependency with p2
if
some NAC in p2
turns satisfied after the aplication of p1
findAllDeliverDelete :: (DPO m, EpiPairs m) => MorphismsConfig -> Production m -> Production m -> [CriticalSequence m] Source #
All DeliverDelete caused by the derivation of p1
before r
.
Rule p1
causes a deliver-delete dependency with p2
if
rule p2
deletes something that is used by p2
,
Verify the non existence of h12: L1 -> D2 such that d2 . h12 = m1'.
findAllForbidProduce :: (DPO m, EpiPairs m) => MorphismsConfig -> Production m -> Production m -> [CriticalSequence m] Source #
All ForbidProduce caused by the derivation of p1
before p2
.
Rule p1
causes a forbid-produce dependency with p2
if some
NAC in right of p1
turns satisfied after the aplication of p2
.
findAllDeliverDangling :: (DPO m, EpiPairs m) => MorphismsConfig -> Production m -> Production m -> [CriticalSequence m] Source #
All DeliverDangling caused by the derivation of p1
before p2
.
Rule p1
causes a deliver-delete dependency with p2
if
rule p2
creates something that disables the inverse of p1
.
findAllProduceUseAndRemoveDangling :: (EpiPairs m, DPO m) => MorphismsConfig -> Production m -> Production m -> [CriticalSequence m] Source #
Tests ProduceUse and RemoveDangling for the same pairs, more efficient than deal separately.