LTLAutomizer Problems

[maul-esel]

As discussed, I'm opening an issue for my problems with LTLAutomizer. I've committed some workarounds and potential fixes in the wip/dk/ltl-fixes branch.

I'm using the following Boogie program:

var x : bool;
var y : bool;

procedure ULTIMATE.start() returns ()
modifies x, y;
{
  havoc y;
  if (y) {
    return;
  }
  
  call P1();
}

procedure P1()
modifies x, y;
{
  if (*) {
    y := true;
  }
  if (!x) {
    x := true;
  }
}

with the LTLAutomizer.xml toolchain and the settings in example/settings/ltlAutomizer/Default.epf. The only change in settings is this:

/instance/de.uni_freiburg.informatik.ultimate.ltl2aut/Read\ property\ from\ file=false
/instance/de.uni_freiburg.informatik.ultimate.ltl2aut/Property\ to\ check= F AP(x)

Problem 1: GotoEdges

This results in:

The Plugin de.uni_freiburg.informatik.ultimate.buchiprogramproduct has thrown an exception:
java.lang.UnsupportedOperationException: BuchiProgramProduct does not support RCFGEdges of type GotoEdge
	at de.uni_freiburg.informatik.ultimate.buchiprogramproduct.productgenerator.ProductGenerator.createEdgesProduct(ProductGenerator.java:373)

This can be avoided by setting

/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Remove\ goto\ edges\ from\ RCFG=true

so this should probably be in the default settings.

Problem 2: NullPointerException with Procedures

With these settings, the next problem is:

The Plugin de.uni_freiburg.informatik.ultimate.plugins.blockencoding has thrown an exception:
java.lang.NullPointerException
	at de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaBuilder.constructCopy(TransFormulaBuilder.java:456)
	at de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.ActionUtils.constructCopy(ActionUtils.java:69)
	at de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transformations.IcfgDuplicator.createUnconnectedCopy(IcfgDuplicator.java:184)
	at de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transformations.IcfgDuplicator.createEdgeCopy(IcfgDuplicator.java:171)
	at de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transformations.IcfgDuplicator.copy(IcfgDuplicator.java:132)
	at de.uni_freiburg.informatik.ultimate.plugins.blockencoding.BlockEncodingObserver.process(BlockEncodingObserver.java:98)

because the copied action is a StatementSequence (a single assume true), whose TransFormula is null. This seems related to procedures, as this statement is a transition from ULTIMATE.startFINAL_NONWA to ULTIMATE.startEXIT_NONWA; and when I use inlining this problem does not occur.

Problem 3: ConcurrentModificationException

I've also encountered the following exception:

The Plugin de.uni_freiburg.informatik.ultimate.buchiprogramproduct has thrown an exception:
java.util.ConcurrentModificationException
	at java.util.HashMap$HashIterator.nextNode(HashMap.java:1445)
	at java.util.HashMap$KeyIterator.next(HashMap.java:1469)
	at de.uni_freiburg.informatik.ultimate.buchiprogramproduct.productgenerator.ProductGenerator.pruneNonProductSinks(ProductGenerator.java:456)
	at de.uni_freiburg.informatik.ultimate.buchiprogramproduct.productgenerator.ProductGenerator.<init>(ProductGenerator.java:154)
	at de.uni_freiburg.informatik.ultimate.buchiprogramproduct.BuchiProductObserver.finish(BuchiProductObserver.java:96)

This problem seems to also be avoided / masked when inlining. I have not yet managed to produce a small example program exhibiting this, and I don't want to post the original program here (student's work; but I can send it to you). The problem seems to be that pruneNonProductSinks iterates over the set mHelperProductStates, and in the iteration calls removeProductProgramPointAndSuccessors (through pruneNonProductSink), which modifies the set.

[maul-esel]

Update: Why Inlining solves all (and none of the) problems

When inlining is turned on, all code is inlined in ULTIMATE.start. LTLAutomizer does not analyse anything in that procedure. This is also a problem in the existing LTLAutomizerCInline.xml toolchain – every property seems satisfied.

To fix this, inlining inside ULTIMATE.start should be turned off. The existing settings seem to only support blacklists for the callee ("do not inline calls to X"), not the caller ("do not inline calls from X").