b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederDescription : Basic analysis for propositional logic extended with QBFs
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederCopyright : (c) Jonathan von Schroeder, DFKI GmbH 2010
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederMaintainer : jonathan.von_schroeder@dfki.de
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederStability : experimental
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederPortability : portable
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederBasic and static analysis for propositional logic
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder <http://en.wikipedia.org/wiki/Propositional_logic>
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder basicPropositionalAnalysis
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , mkStatSymbItems
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , mkStatSymbMapItem
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , inducedFromMorphism
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , inducedFromToMorphism
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , signatureColimit
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport qualified Common.AS_Annotation as AS_Anno
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport qualified Common.GlobalAnnotations as GlobalAnnos
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport qualified Common.Id as Id
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport qualified Common.Result as Result
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport qualified Data.List as List
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport qualified Data.Map as Map
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport qualified Data.Set as Set
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport qualified QBF.AS_BASIC_QBF as AS_BASIC
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport qualified QBF.Morphism as Morphism
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport qualified QBF.Symbol as Symbol
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Datatype for formulas with diagnosis data
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederdata DIAGFORM = DiagForm
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder formula :: AS_Anno.Named AS_BASIC.FORMULA,
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Formula annotated with a number
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederdata NUMFORM = NumForm
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder nfformula :: AS_Anno.Annoted AS_BASIC.FORMULA
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , nfnum :: Integer
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederdata TESTSIG = TestSig
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , occurence :: Int
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Retrieves the signature out of a basic spec
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -> Sign.Sign -- Input Signature
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder -> TESTSIG -- Output Signature
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroedermakeSig (AS_BASIC.BasicSpec spec) sig = List.foldl retrieveBasicItem
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder TestSig { msign = sig
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , occurence = 0
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , tdiagnosis = []
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- Helper for makeSig
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederretrieveBasicItem ::
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder TESTSIG -- Input Signature
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder -> AS_Anno.Annoted AS_BASIC.BASICITEMS -- Input Item
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder -> TESTSIG -- Output Signature
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederretrieveBasicItem tsig x =
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder occ = occurence tsig
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (\ asig ax -> TestSig {
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder msign = Sign.addToSig (msign asig)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , occurence = occ
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , tdiagnosis = tdiagnosis tsig ++
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder tsig $ (\ (AS_BASIC.PredItem xs _) -> xs) apred
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (\ asig ax -> TestSig {
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder msign = Sign.addToSig (msign asig)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , occurence = occ
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , tdiagnosis = tdiagnosis tsig ++
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder "Definition of proposition " ++
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder show (pretty ax) ++
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder " after first axiom"
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder tsig $ (\ (AS_BASIC.PredItem xs _) -> xs) apred
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (AS_BASIC.AxiomItems _) -> TestSig { msign = msign tsig
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , occurence = occ + 1
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , tdiagnosis = tdiagnosis tsig ++
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Retrieve the formulas out of a basic spec
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroedermakeFormulas (AS_BASIC.BasicSpec bspec) sig =
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder List.foldl (\ xs bs -> retrieveFormulaItem xs bs sig) [] bspec
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- Helper for makeFormulas
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederretrieveFormulaItem ::
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder -> AS_Anno.Annoted AS_BASIC.BASICITEMS
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederretrieveFormulaItem axs x sig =
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder List.foldl (\ xs bs -> addFormula xs bs sig) axs $ numberFormulae ax 0
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- Number formulae
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroedernumberFormulae :: [AS_Anno.Annoted AS_BASIC.FORMULA] -> Integer -> [NUMFORM]
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedernumberFormulae [] _ = []
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroedernumberFormulae (x : xs) i
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder | label == "" =
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder NumForm {nfformula = x, nfnum = i} : numberFormulae xs (i + 1)
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder NumForm {nfformula = x, nfnum = 0} : numberFormulae xs i
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder-- Add a formula to a named list of formulas
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederaddFormula :: [DIAGFORM]
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederaddFormula formulae nf sign
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder | isLegal = formulae ++
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder formula = makeNamed f i
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder | otherwise = formulae ++
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder formula = makeNamed f i
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder "Unknown propositions "
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder ++ show (pretty difference)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder ++ " in formula "
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder ++ show (pretty nakedFormula)
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder f = nfformula nf
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder varsOfFormula = propsOfFormula nakedFormula
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder isLegal = Sign.isSubSigOf varsOfFormula sign
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder difference = Sign.sigDiff varsOfFormula sign
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- generates a named formula
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroedermakeNamed :: AS_Anno.Annoted AS_BASIC.FORMULA -> Integer
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedermakeNamed f i = (AS_Anno.makeNamed (if label == "" then "Ax_" ++ show i
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder { AS_Anno.isAxiom = not isTheorem }
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder isImplies = foldl (\ y x -> AS_Anno.isImplies x || y) False annos
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder isImplied = foldl (\ y x -> AS_Anno.isImplied x || y) False annos
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder isTheorem = isImplies || isImplied
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- Retrives the signature of a formula
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederpropsOfFormula :: AS_BASIC.FORMULA -> Sign.Sign
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederpropsOfFormula (AS_BASIC.Negation form _) = propsOfFormula form
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederpropsOfFormula (AS_BASIC.Implication form1 form2 _) = Sign.unite
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (propsOfFormula form1)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder (propsOfFormula form2)
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederpropsOfFormula (AS_BASIC.Equivalence form1 form2 _) = Sign.unite
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (propsOfFormula form1)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder (propsOfFormula form2)
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederpropsOfFormula (AS_BASIC.TrueAtom _) = Sign.emptySig
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederpropsOfFormula (AS_BASIC.FalseAtom _) = Sign.emptySig
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederpropsOfFormula (AS_BASIC.Predication x) = Sign.Sign
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederpropsOfFormula (AS_BASIC.Conjunction xs _) = List.foldl
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder (\ sig frm -> Sign.unite sig $ propsOfFormula frm)
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederpropsOfFormula (AS_BASIC.Disjunction xs _) = List.foldl
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder (\ sig frm -> Sign.unite sig $ propsOfFormula frm)
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederpropsOfFormula (AS_BASIC.ForAll xs f _) = sigDiff
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (propsOfFormula f)
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (Sign.Sign (Set.fromList (map Id.simpleIdToId xs)))
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederpropsOfFormula (AS_BASIC.Exists xs f _) = sigDiff
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (propsOfFormula f)
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (Sign.Sign (Set.fromList (map Id.simpleIdToId xs)))
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- Basic analysis for propositional logic
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederbasicPropositionalAnalysis
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder :: (AS_BASIC.BASICSPEC, Sign.Sign, GlobalAnnos.GlobalAnnos)
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder -> Result.Result (AS_BASIC.BASICSPEC,
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederbasicPropositionalAnalysis (bs, sig, _) =
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Result.Result diags $ if exErrs then Nothing else
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Just (bs, ExtSign sigItems declaredSyms, formulae)
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder bsSig = makeSig bs sig
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder sigItems = msign bsSig
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder $ Set.difference (items sigItems) $ items sig
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder bsForm = makeFormulas bs sigItems
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder formulae = map formula bsForm
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder diags = map diagnosis bsForm ++ tdiagnosis bsSig
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Static analysis for symbol maps
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroedermkStatSymbMapItem :: [AS_BASIC.SYMBMAPITEMS]
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -> Result.Result (Map.Map Symbol.Symbol Symbol.Symbol)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedermkStatSymbMapItem xs =
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Map.union smap $ statSymbMapItem sitem
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederstatSymbMapItem :: [AS_BASIC.SYMBORMAP]
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -> Map.Map Symbol.Symbol Symbol.Symbol
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederstatSymbMapItem =
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (symbToSymbol sym)
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (symbToSymbol sym) mmap
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -> Map.insert (symbToSymbol s1) (symbToSymbol s2) mmap
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Retrieve raw symbols
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroedermkStatSymbItems :: [AS_BASIC.SYMBITEMS] -> Result.Result [Symbol.Symbol]
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedermkStatSymbItems a = Result.Result
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , Result.maybeResult = Just $ statSymbItems a
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederstatSymbItems :: [AS_BASIC.SYMBITEMS] -> [Symbol.Symbol]
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederstatSymbItems = concatMap symbItemsToSymbol
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroedersymbItemsToSymbol :: AS_BASIC.SYMBITEMS -> [Symbol.Symbol]
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroedersymbItemsToSymbol (AS_BASIC.SymbItems syms _) = map symbToSymbol syms
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedersymbToSymbol :: AS_BASIC.SYMB -> Symbol.Symbol
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroedersymbToSymbol (AS_BASIC.SymbId tok) =
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder Symbol.Symbol {Symbol.symName = Id.simpleIdToId tok}
ba06b25b69be05a4733db7197940efd73976f215Jonathan von SchroederpMap :: Map.Map Symbol.Symbol Symbol.Symbol -> Set.Set Id.Id
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Induce a signature morphism from a source signature and a raw symbol map
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederinducedFromMorphism :: Map.Map Symbol.Symbol Symbol.Symbol
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederinducedFromMorphism imap sig =
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder , Morphism.propMap = pMap imap sigItems
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder (pMap imap sigItems))
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Induce a signature morphism from a source signature and a raw symbol map
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederinducedFromToMorphism :: Map.Map Symbol.Symbol Symbol.Symbol
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederinducedFromToMorphism imap (ExtSign sig _) (ExtSign tSig _) =
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder (pMap imap sigItems))
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder isSub = Sign.items targetSig
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder , Morphism.propMap = pMap imap sigItems
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder "Incompatible mapping"
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedersignatureColimit :: Gr Sign.Sign (Int, Morphism.Morphism)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -> Result.Result (Sign.Sign, Map.Map Int Morphism.Morphism)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedersignatureColimit graph = do
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder let graph1 = nmap Sign.items $ emap (Control.Arrow.second Morphism.propMap)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder (set, maps) = addIntToSymbols $ computeColimitSet graph1
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder Map.fromList $ map (\ (i, n) ->
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder })) $ labNodes graph)