verigraph-1.1.1: Software specification and verification tool based on graph rewriting.

Safe HaskellSafe
LanguageHaskell2010

Analysis.CriticalPairs

Contents

Synopsis

Documentation

data CriticalPair m Source #

A Critical Pair is defined as two matches (m1,m2) from the left side of their rules to a same graph. It assumes that the derivation of the rule with match m1 causes a conflict with the rule with match m2

This diagram shows graphs and morphisms names used in the algorithms below

p1 = production (L1,K1,R1,[N1])

p2 = production (L2,K2,R2,[N2])

                   N1    N2
                   ^      ^
         r     l   │      │n
    R1◀─────K1────▶L1    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

Constructors

CriticalPair 

Fields

getCriticalPairMatches :: CriticalPair m -> (m, m) Source #

Returns the matches (m1,m2)

getCriticalPairComatches :: CriticalPair m -> Maybe (m, m) Source #

Returns the comatches (m1',m2')

getNacMatchOfCriticalPair :: CriticalPair m -> Maybe m Source #

Returns the nac match of a CriticalPair

getCriticalPairType :: CriticalPair m -> CriticalPairType Source #

Returns the type of a Critical Pair

Finding Critical Pairs

findCriticalPairs :: (EpiPairs m, DPO m) => MorphismsConfig -> Production m -> Production m -> [CriticalPair m] Source #

Finds all Critical Pairs between two given Productions

findPotentialCriticalPairs :: (DPO m, EpiPairs m) => MorphismsConfig -> Production m -> Production m -> [(m, m)] Source #

Returns a list of morphisms from left side of rules to all valid overlapping pairs

namedCriticalPairs :: (EpiPairs m, DPO m) => MorphismsConfig -> [NamedRule m] -> [NamedCriticalPairs m] Source #

Returns the Critical Pairs with rule names

findAllDeleteUse :: (EpiPairs m, DPO m) => MorphismsConfig -> Production m -> Production m -> [CriticalPair m] Source #

All DeleteUse caused by the derivation of p1 before p2. It occurs when p1 deletes something used by p2.

findAllProduceForbid :: (EpiPairs m, DPO m) => MorphismsConfig -> Production m -> Production m -> [CriticalPair m] Source #

All ProduceForbid caused by the derivation of p1 before p2.

Rule p1 causes a produce-forbid conflict with p2 if some NAC in p2 fails to be satisfied after the aplication of p1.

findAllProduceDangling :: (EpiPairs m, DPO m) => MorphismsConfig -> Production m -> Production m -> [CriticalPair m] Source #

All ProduceDangling caused by the derivation of p1 before p2. It occurs when p1 creates something that unable p2.

findAllDeleteUseAndProduceDangling :: (EpiPairs m, DPO m) => MorphismsConfig -> Production m -> Production m -> [CriticalPair m] Source #

Tests DeleteUse and ProduceDangling for the same pairs, more efficient than deal separately.