Dosiahnutelnost v orientovanom grafe G = (V, E)

• pociatocný vrchol: init

  1. vrchol init je dosiahnutelný
  
  2. Ak u je dosiahnutelný a (u, v) je hrana, tak aj v je dosiahnutelný
  3. ziaden iný nie je dosiahnutelný

• r[v] je true, ak vrchol v je dosiahnutelný:

  ? ? v: v ? V :: r[v] ? vrchol v je dosiahnutelný ?
  

• invariant

  ? ? v: v ? V :: r[v] ? v je dosiahnutelný ? ? r[init]
  

• FP ? ? ? u, v: (u, v) ? E :: r[u] ? r[v] ?

FP ? ? ? u, v: (u, v) ? E :: r[u] ? (r[u] ? r[v]) ?

pretoze r[u] ? (r[u] ? r[v]) ? (r[u] ? r[v])

• platnost invariantu zarucíme, ak na zaciatku bude

  r[v] = false, teda v ? init
  

• Program Reach

  declare r: array[V] of boolean
  
  initially ?  v: v ? V :: r[v] = (v = init) ?
  assign ?  u, v: (u, v) ? E :: r[u] := r[u] ? r[v] ?

end{Reach}

• dá sa dokázat, ze pre metriku M platí:

  M = |{ v | ?r[v] }|
  

Previous slide

Next slide

Back to first slide

View graphic version