module parcelrouter // Component abstract signature abstract sig Component { output : set Component, // zero or more outputs parcel : lone Parcel // zero or one parcel } { lone this.~@output // a component has at most one parent !(this in this.^@output) // no cyclic reference } // Generator signature extending Component sig Gen extends Component { firstOutput : output // exactly one first output } { firstOutput = output // ensures that a generator has only one output that is the first ouput firstOutput in Stage // the component directly after the generator is a stage no this.~@output // a generator has no parent } // Stage signature extending Component sig Stage extends Component { leftOutput : output, // exactly one left output rightOutput : output // exactly one right output } { output = leftOutput + rightOutput // ensures that a stage has only two outputs leftOutput != rightOutput // the two outputs are different one gen : Gen | gen in this.~^@output // ensures that all stages are accessible from one generator (leftOutput + rightOutput) in Bin or (leftOutput + rightOutput) in Stage // ensures the parcel router is a binary tree } // Bin signature extending Component sig Bin extends Component { tag : Tag // exactly one tag } { one this.~@output // a bin has exactly one parent no output // a bin has no output } // Tag signature sig Tag { } { one this.~@tag // a tag has exactly one parent bin // Note that this fact in addition to the tag field of Bin (with multiplicity one for each) // ensures that there will be exactly the same number of tags and bins // and also ensures that each bin has a different tag } // Parcel signature sig Parcel { tagP : Tag // exactly one tag } { one this.~@parcel // exactly one component contains the parcel } // Check whether tags can be shared or not assert TagCannotBeShared { all disj b1,b2:Bin | b1.tag != b2.tag } // Ensures the correct positionning of a parcel according to the bins' tags fact EnforcePositionOfParcel { all p : Parcel | let comp = p.~parcel | ((comp in Bin) implies comp.tag = p.tagP) and ((comp in Stage) implies p.tagP in comp.^output.tag) } // Enforce the position of the parcel inside the generator pred generate { one p: Parcel | one g: Gen | g.parcel = p } /* The predicate below simulates the transmission of a parcel into a successor component. The parameter c represents the current component where the parcel is and from which the parcel has to be transmitted to the successor component of c. Two cases: - the current component is the Generator, then this predicate must enfore that the parcel is transmitted to the first stage; - the current component is a Stage, then this predicate must enfore that the parcel is transmitted to the next component (that can be either a Stage or a Bin) We do not consider the case where component is a Bin as the bin as no successor. */ pred transmitParcel[c : Component] { // To complete } /* The predicate below ensures that the parcel is always inside the Generator. To try the above predicate, you can comment the 'generate' line and successively test the three last lines. */ pred Show { one Parcel one Gen generate // one g : Gen | transmitParcel[g] // one g : Gen | transmitParcel[g.output] // #Stage = 3 and one g : Gen | transmitParcel[g.output.leftOutput] } run Show for 8 check TagCannotBeShared for 8