Here is a first file sc-loc-bis.cat that exactly follows the
observation.
"SC per location"
// Define the coherence (co) relation
include "cos.cat"
// Communication relations
let com = rf|co|fr
// Consistency condition for SC
irreflexive po;com+ as SC-LOC
Yet another formulation stems from the remark that the transitive
closure of communication relations can be expressed as the union of
five cases:
\let complus = rf | co | fr | (fr;rf) | (co;rf)
This results from co begin transitive and from
fr;co being included in fr (by definiton of
fr).
A second model sc-loc-ter.cat follows from this alternative
formulation of complus.
"SC per location"
// Define the coherence (co) relation
include "cos.cat"
// Transitive communication relations
let complus = rf | co | fr | fr;rf | co;rf
// Consistency condition for SC
irreflexive po;complus as SC-LOC