Rethink transformation of edges containing guards with clock variables in the XSTS-UPPAAL transformer

[bnctth]

In the current solution, we first generate the UPPAAL model from the XSTS model without any regard to clocks, perform optimizations on it, then post-process it the following way:

1. Check if the expression contains an OR expression (at any depth), where on either side we reference a clock variable (also at any depth)
2. If yes, then we map our current expression's top level component the following way:
   • ANDs become an intermediate location, with the operands split between the incoming and outgoing edge
   • ORs become parallel edges with the operands split between them
3. Recursively run step 1 on both created edges.

While this method works, it outputs models with an excessive amount of extra locations and edges, making verification slower. My PR takes a completely different approach.

Handling clock references becomes part of the XSTS to UPPAAL transformation step. Guard expressions are processed by ClockGuardTransformer. It brings the expression into DNF form only for clock references, meaning the top level OR's operands are going to be a conjunction of clock comparisons and any non-clock expressions. These operands become guards on parallel edges. As an additional optimization, operands that are definitely false don't produce edges.

[grbeni]

License is missing

[grbeni]

I few thoughts:

• I left some programming specific comments.
• "it outputs models with an excessive amount of extra locations and edges, making verification slower" is a strong statement. Could you provide examples (see examples folder in the repo) where your approach is (significantly) faster?
• Manytimes, it turns out that different solutions (i.e., the current one and your new one) are efficient for different models, so making this configurable would be a big plus (e.g., by using a boolean attribute). Of course, if you prove that your solution is always better, then there is no need for this. :)
• We need tests (see tests folder in the repo) for this PR to be merged, where you show that this solution is actually works as expected.

[bnctth]

I checked out the tests folder (both validation-model-suite and model), I saw the models, but I'm not sure how to provide an expected output and have it checked. Could you please explain it to me? In the meantime I'm working on the requested benchmarks.