Total Order checking in Properties.cpp

[viraj96]

Hi,

I was going through the code base and I could not understand one thing in the properties.cpp file. In isTopSortTotalOrder I believe the intention is to check whether the topological sort returned by the liftedPropertyTopSort function has total ordering or not? If yes then why is there a break statement inside the if condition? I feel that for the orderEnforced variable to be true, the if condition is required to be met by all the orderings. Please correct me if I understood this incorrectly!

[galvusdamor]

Hi,

What I am testing here is whether for every two immediately neighbouring elements (i and i-1) of the topological ordering, the order between them is actually enforced. This is the case if the edge (i-1,i) exists. I.e. I am just checking whether the edge exists or not and can thus abort if I have found it.

The logic here is as follows: if the method is totally-ordered, then its topological ordering is unique (well it must be that total ordering). If it is unique, then every two tasks in the order that follow immediately after one another, there must be an ordering constraint. If not, I could swap them and the order would not be unique any more (i.e. I would not have a total ordering). On the other hand, if I have a non-totally-ordered method, then such a pair of tasks must exist in any arbitrarily chosen topological ordering.

Kind regards, Gregor

[viraj96]

Thanks! That clears it for me!