| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
Analysis.CriticalSequence
Contents
- 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
Constructors
| 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 |
Instances
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
Instances
| 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.