LTLAutomizer Problems - Githubissues

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.

ultimate-pa / ultimate

LTLAutomizer Problems #508

Problem 1: GotoEdges

Problem 2: NullPointerException with Procedures

Problem 3: ConcurrentModificationException

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