Recent changes to bugs

[](Fluent) is not working well

2015-05-05T03:26:06.674000Z

When we make set a as a safety goal. The machine obtained is the same when the Fluent is initially 0 or 1. They should be different machines.

For example:

Fluent OnInitiallyFalse = <on,off> initially 0
Fluent OnInitiallyTrue = <on,off> initially 1

Both machines are the same.

Pessimistic is distributed if applied to a merge

2009-05-11T13:48:08Z

pessimistic C = (A ++ B).
The tool is doing pessimistic A, then pessimistic B and after that trying to merge.
It should perform the merge and then get the pessimistic model.

Minimal - Bug and inconsistency

2009-04-01T13:44:42Z

Check the attached file.
minimal ||It2_PostMin = (It1_Resulting_MTS).
minimal ||It2Min = (It1).
It1 = (OrderFood ++ UpdateStock).

It1_Resulting_MTS is just the result of the merge in It1 (copy and pasted from the Transition window). So technically they are the same.
It2_PostMin is minimised and the result is verified as correct. However It2Min is minimised but the minimised and the original are not comparable (they have a different alphabet). They should be comparable, and also, It2Min and It2_PostMin should lead to the same resulting MTS (or both raise an exception).

Cannot see model names in refinement dialog box

2009-03-27T17:08:46Z

On my mac, if you go to the refiement option in MTS menu, the dialog box that appears which lets you pick to models wich are to be compared uses drop down menus which only let me see the first few letters of the model names.

Invalid result with strong refinement

2009-03-27T17:06:36Z

Checking strong refinement, the tool does not abort if the models have different alphabets. Should say: Not applicable.

Index out of bound exception when minimising

2009-02-27T12:19:03Z

When merging and then minimising like "minimal ||Itl_Aux1_P3 = (Itl_Aux1_Env ++ C_P3)." an IndexOutOfBoundException is thrown.
However if using minimal on the pre calculated merge there is no such exception.
See attached file.

Combining minimal and optimistic has no clear meaning

2009-02-17T12:35:55Z

Combining minimal and optimistic behaves differently when applied to a process than when applied to a composition.
When used on a simple MTS processes the optimistic version is first calculated and then minimised (LTS minimisation).
When used on a composite MTS the MTS minimisation is used (and the optimistic is not calculated) (MTS minimisation).

For example:

minimal optimistic MTS1 = ... // (FSP process definition). Calculates the optimistic MTS and then minimises it (LTS minimisation)
minimal optimistic ||MTS2 = (MTS1). // minimises MTS1 (MTS minimisation). No optimistic version is calculated.
minimal optimistic ||MTS3 = (MTS1 ++ AnotherMTS). // minimises the merged MTS (MTS minimisation). No optimistic version is calculated.

Safety checks: unexplained requirement

2009-02-16T16:53:00Z

Why does there have to be a deadlock free implementation to do a safety checks? (Note that this is the check against an observer, it is not referring to checks against FLTL safety properties)

Suspect behaviour of minimization

2009-02-16T16:50:10Z

With all the changes regarding refinement, it would only be natural to have problems with minimization.
We should have at least a sanity check at the end of it where the resulting minimized MTS is checked for equivalence against the original.

Weird code in checkSafety()

2009-02-16T16:44:56Z

WHy does it say "there must be a property to check"