Fix/inconsistent location invariant

[Brandhoej]

Fixes #62 where the inconsistent location has an incorrect invariant. The fix for this was to introduce a global clock which, upon creation of a Quotient instance, is searched for. If this clock exists then it is reused in a new inconsistent location otherwise one is created. Also, flaky tests were happening as some tests at random times tried to reduce a terminal CDD this has been fixed by adding several checks in CDD for shortcut computations.

Description

• Quotient: Now reuses clock used by inconsistent locations.
• UniqueNamedContainer: Has been updated to allow for global named items in its collection.
• Automaton: Making an automaton input enabled has been refactored and terminal CDD, which could be encountered, are now handled gracefully. With the additions in CDD I don't think the isTerminal check is required, but I still prefer having it.
• QuotientTest: Now has tests to check whether clocks are being reused.

Opens

• I think the introduction of global clocks introduce the requirement for explicitly designing our scope rules.
• Instead of using names for an Automaton I think we should use a symbol from a symboltable.

Related Issues

Closes #62

[magoorden]

I have done a round of review.

For next time: reviews are (in general) easier when they are smaller. Now you solve multiple issues in the same merge request.

[ulriknyman]

I think it is dangerous to allow spaces in names. I think we should stick to having _ (underscores in the names).

--ulrik On 05/02/2023 08.56, Andreas K. Brandhøj wrote: @Brandhoej commented on this pull request.

________________________________ In src/logic/Refinement.java<#94 (comment)>:

@@ -432,8 +432,9 @@ private boolean checkActions(State state1, State state2, boolean isInput) {

Log.debug("create pairs failed"); if (RET_REF) { - Location ll = Location.createInconsistentLocation("inconsistent", 0, 0); - Location rl = Location.createInconsistentLocation("inconsistent", 0, 0); + Clock inconsistentClock = new Clock("inconsistent clock", "refinement"); I don't know how parsing is affected by spaces in names, but I would prefer to allow them. — Reply to this email directly, view it on GitHub<#94 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/ADBJZC23UDCI6PYWGUQP7CDWV5MLDANCNFSM6AAAAAASOQYU7Y>. You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

…

-- ⬡ Ulrik Nyman, http://ulrik.blog.aau.dk, mobile: (+45) 40 89 21 56 ⩽ Associate Professor, Ph.D. Head of Studies at Department of Computer Science Deputy Head of Department, http://www.cs.aau.dk Education Coordinator for Software Aalborg University, http://www.aau.dk

[magoorden]

Thanks for the improvement. Just some minor stuff I noticed.