| Policy
invariants |
|
|
|
|
|
|
|
|
|
|
| • | Place
a gate wherever there is a conflict |
||||||||
| inv
GatePlacement { |
|||||||||
| all s | some s.conflicts -> some
s.gate |
|||||||||
| } |
|||||||||
| • | At
most one open gate in a conflicting |
||||||||
| group |
|||||||||
| inv Policy { |
|||||||||
| all s | sole (s.conflicts + s).gate
& Open |
|||||||||
| } |
|||||||||
