Add exclusiveWith for transactions

[amascare]

It would be great to be able to have mutually exclusive transactions like done for the applications. This would allow us to work at a lower level of granularity, which helps to be more precise in some cases.
For example, t_a exclusiveWith t_b.

[Gaudeval]

It can be done.

Understand that exclusiveWith is an interference view operator, so it can only be used during interference rules specification for transactions (respectively applications) in the definition of a PhysicalTableBasedInterferenceSpecification (respectively ApplicativeTableBasedInterferenceSpecification).

We consider the former case, specifying interference for transactions. The process is the following:

1. Specify interference rules on transactions: We declare a trait that extends PhysicalTableBasedInterferenceSpecification.
2. Configure the platform to view transactions: We specify the platform to which the specification applies (standard in PML), and configure the platform with a software and a transaction library (not as standard here).
3. Tag two transactions as exclusive: We tag each transaction as used and retrieve its concrete counterpart. Then we can call the exclusiveWith operator on both concrete transactions.
4. Repeat 3. as required

/* 1. Specify interference rules on transactions */
trait MyPhysicalTableBasedInterferenceSpecification extends PhysicalTableBasedInterferenceSpecification {
  /* 2. Configure the platform to view transactions. */
  self: SimpleKeystonePlatform with SimpleSoftwareAllocation with SimpleKeystoneTransactionLibrary =>
  /* ... */

  /* 3. Tag two transactions as exclusive */
  for {
    /* Tag each transaction as used, and retrieve its counterpart */
    l <- t12_app1_rd_d1.used.toPhysical 
    r <- t221_app22_rd_d2.used.toPhysical
  } yield {
      l exclusiveWith r /* Tag the selected transactions as exclusive */
  }

@kevin-delmas , I am conscious this is quite an inelegant workaround. I might ping you to discuss how to add an operator on Transaction that does just this.

[kevin-delmas]

The workaround of @Gaudeval is indeed a solution.
We do not consider exclusive operator on User Transactions.
@amascare Would you like to directly tag User Transactions as exclusive that is

 t12_app1_rd_d1 exclusiveWith t221_app22_rd_d2

If so, this may request an additional development to be scheduled.

[amascare]

Thank you @Gaudeval and @kevin-delmas.
I think it would be a good idea to have it in the future for the sake of simplicity, especially in complex systems. However, I would say that is not a priority as the workaround provided by @Gaudeval is functional.

[kevin-delmas]

Ok then, we add that to the scheduled enhancements.
I will see if such simple improvements could be achieved by @ccoquand (with my full support for sure 😉 )