-
Notifications
You must be signed in to change notification settings - Fork 9
Description
There are currently 7 ignored tests.
testRefinementByNiels: Is non-deterministic. The CI nearly always have this test pass, but on my local development PCs it fail 90% of the time. The assertions which fails are assert(new SimpleTransitionSystem(auts[1]).isFullyConsistent()); and assert(new SimpleTransitionSystem(auts[1]).isLeastConsistent());. When removing the assert(new SimpleTransitionSystem(auts[1]).isDeterministic()); they still fail meaning that the isDeterminsitic check does not alter the state of the automaton.
Z2RefinesZ2Z3Z4: Z2 <= Z2 \\ Z3. Fails refinement because Z2 has output oand Z2 \\ Z3 has the same as input. Both Z2 and Z3 have no inputs and only o as an output. As the quotient inputs are Act_i^T ∪ Act_o^S o will always be an input of the quotient. Either this test is incorrect or the channel o should be distinct between Z2 and Z3.
testBoolSafeLoadXML: Relies on files from the testOutput directory which cannot be found when running the tests.
T0RefinesT3T1T2: Fails on two refinements (T3 \\ T4) \\ T2 <= (T3 \\ T4) \\ T2 and T1 <= (T3 \\ T4) \\ T2. The first assertion fails because of Output violation and the second because of a Delay violation.
newQuotientTest5: Fails because the file comp.xml cannot be found.
testFromTestFramework1: Fails refinement on Machine <= ((((Adm2 && HalfAdm1) || Machine || Researcher) \\ (Adm2 && HalfAdm2)) \\ Researcher) but a test passes on Machine <= (Machine || ((Adm2 && HalfAdm1) || Researcher)) \\ ((Adm2 && HalfAdm2) || Researcher).
testFromTestFramework2: Fails refinement on Administration <= (Spec \\ Machine) \\ Researcher but a test passes on Administration <= (Spec \\ (Machine || Researcher)).