Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Possibly incorrect tests #79

Open
Brandhoej opened this issue Oct 23, 2022 · 1 comment
Open

Possibly incorrect tests #79

Brandhoej opened this issue Oct 23, 2022 · 1 comment
Labels
bug Something isn't working help wanted Extra attention is needed invalid This doesn't seem right question Further information is requested

Comments

@Brandhoej
Copy link
Contributor

Brandhoej commented Oct 23, 2022

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)).

@Brandhoej Brandhoej mentioned this issue Oct 23, 2022
@Brandhoej Brandhoej added bug Something isn't working help wanted Extra attention is needed invalid This doesn't seem right question Further information is requested labels Oct 23, 2022
@magoorden
Copy link
Contributor

Fixed some small typo's in the issue discription.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working help wanted Extra attention is needed invalid This doesn't seem right question Further information is requested
Projects
None yet
Development

No branches or pull requests

2 participants