TableBasedInterferenceSpecification

Map from the physical transaction id and their service sequence representation computed through an analysis of the platform WARNING: this lazy variable MUST NOT be called during platform object initialisation

Map from the service sequence representation to their id WARNING: this lazy variable MUST NOT be called during platform object initialisation

Set gathering discarded transactions

compute the considered scenarios depending on the configuration and the (optional) library, a scenario is either: a named and used transaction (e.g. val t = Transaction(a read b); t.used) a named and used scenario (e.g. val s = Scenario(t1, t2); s.used) an anonymous copy (e.g. a copy r on s) an anonymous transaction (e.g. a read b) not already involved in a copy, a named scenario or a named transaction WARNING this will discard an anonymous transaction defined inside and outside a copy, this issue does not occur if we keep the segregation Smart/NonSmart

Relation gathering user defined equivalent services

Relation gathering user defined interfering hardware

Relation gathering user defined non-interfering hardware

Relation gathering user defined service interferences caused by a transaction

Relation gathering user defined service non-interference caused by a transaction

Relation gathering user defined service interferences

Relation gathering user defined service non-interferences

Provide the map encoding of finalInterfereWith

Check whether two scenarios will not occur simultaneously

Check whether two transaction will not occur simultaneously

Provide the equivalence classes over s with views.interference.operators.Equivalent.Ops relation

Provide the equivalence classes over s with views.interference.operators.Equivalent.Ops relation

Provide the map encoding of channelNonEmpty

Check if it exists at least one common service used by two set of scenarios

Add the services of transactionInterfereWith to the path and remove the ones of transactionNotInterfereWith

Check if two services interfere with each other

Check whether two hardware cannot work simultaneously

Convert an application to the set of transaction id its trigger

Convert an application to the set of transaction id its trigger

Convert a physical id to the corresponding path of services

Convert a physical id to the corresponding path of services

Relation gather user defined exclusive software

Relation gathering user defined exclusive transactions

The set of services provided by the platform

Derive implementation from serviceEquivalent

Derive implementation from transactionExclusive, swExclusive or same hardware owner

Derive implementation from serviceInterfereWithService

Derive implementation from hardwareExclusive

Derive implementation from transactionIsTransparent

Derive implementation from physicalTransactionIdInterfereWithService

Derive implementation from physicalTransactionIdNotInterfereWithService