Recent changes to bugs

explicit negatives

2008-12-22T18:43:15Z

Currently, the automatically generated PROMELA model does not make negatives explicit - not sure whether this will make a difference for our purposes

debug mode fault

2008-12-22T10:55:56Z

When in debug mode, two dialog boxes are displayed for every question

empty counter examples cause exception

2008-09-01T12:15:59Z

need better way of dealing with empty counter examples - SPIN can provide multiple counter examples, which should provide alternatives.

dot graph output has extra node

2008-08-22T09:38:56Z

When dot-graph output is switched on, the graph has a superfluous node.

exception when using LTL formulae with QSMTool interface

2008-07-31T14:22:16Z

When using the attached file as input to QSMTool (using the LTL extension), I get the following output:

<temp> [c, c]
RESTART - restartSOFT
Configuration file null does not exist.
Exception in thread "RPNI learner thread" java.lang.NullPointerException
at statechum.analysis.learning.rpnicore.ComputeQuestions.computeQS_general(ComputeQuestions.java:88)
at statechum.analysis.learning.rpnicore.ComputeQuestions.computeQS(ComputeQuestions.java:395)
at statechum.analysis.learning.spin.BlueFringeSpinLearner.learnMachine(BlueFringeSpinLearner.java:113)
at statechum.analysis.learning.PickNegativesVisualiser$1.run(PickNegativesVisualiser.java:119)
at java.lang.Thread.run(Thread.java:619)

RandomPathGenerator only produces negative paths

2008-06-19T08:38:52Z

In RandomPathGenerator call the generatePosNeg or generateRandomPosneg methods.

Afterwards, when you call a getAllSequences it returns a set of negative paths, but when you call a getExtraSequences method it is empty.

In practice, it is possible to use the getAllSequences by itself (you can treat the prefixes to the negative strings as positive strings), so doesn't it make sense to just remove the getExtraSequences altogether?

merged pta misses transitions

2008-04-06T12:07:44Z

Using BlueFringeSpinLearner, after a soft restart, the resulting PTA can sometimes miss out important transitions.

I doubt the hard/soft restart issue has anything to do with this bug, it looks as if something might be going wrong during the merging process?

Attached is a screenshot - so here there is only one possible path from Init, with just a single transition, the second transition to the rest of the machine is missing, so it generates no further questions.