Extending the AFA-bits Format for Formulae in General Form?

[jn1z]

This is separate from the high-memory issue; these fail pretty much immediately.

./build/examples/example06-mintermization automata-bench/bench2/ltl_afa/created_ltl/LTLf-specific/Response/N360.mata
... (outputs original file)...
Segmentation fault (core dumped)

[jn1z]

This is happening on line 101 of mintermization.cc:
"if (bdd.val.IsZero())" is crashing.
Printing out the value of bdd.val gives "libMATA error: empty DD."

[Adda0]

Thid will be of great help when debugging the issue. Thank you for the reports.

[koniksedy]

The Bug

The execution fails on line 101 because the previous assertion on line 100 is turned off by the release compilation. This assertion would normally be triggered when bdd.type equals OptionalBdd::TYPE::NOTHING_E.

mata/src/mintermization.cc

Lines 94 to 106 in 8b885af

	// Foreach disjunct create a BDD
	for (const DisjunctStatesPair& ds_pair : lhs_to_disjuncts_and_states[&trans.first]) {
	// create bdd for the whole disjunct
	const auto bdd = (ds_pair.first == ds_pair.second) ? // disjunct contains only states
	OptionalBdd(bdd_mng.bddOne()) : // transition from state to states -> add true as symbol
	graph_to_bdd_afa(*ds_pair.first);
	assert(bdd.type == OptionalBdd::TYPE::BDD_E);
	if (bdd.val.IsZero())
	continue;
	trans_to_bddvar[ds_pair.first] = bdd.val;
	bdds.insert(bdd.val);
	}
	}

Is It Really a Bug?

As can be inferred from the comments and variable names in the for-loop, it deals with some kind of disjuncts (lhs_to_disjuncts_and_states). The variable ds_pair is even of the type DisjunctStatePairs, defined as:

using DisjunctStatesPair = std::pair<const FormulaGraph *, const FormulaGraph *>;

This, along with the fact that the automaton:

@AFA-bits
%Initial qOR2
%Final qI & qOR2
qI \true
qOL1 aV1
qOL2 aV2
qOR2 (qOL1 | qOL2) & qI

leads to an assertion failure on line 100, whereas the automaton:

@AFA-bits
%Initial qOR2
%Final qI & qOR2
qI \true
qOL1 aV1
qOL2 aV2
qOR2 (qOL1 & qI) | (qOL2 & qI)

passes without any problem, suggests that the official automata format accepts formulae only in Disjunctive Normal Form (DNF).

Should We Extend AFA-bits for Formulae in General Form?

This observation raises the question of whether we should extend the AFA-bits automaton format to support transition formulae in general form (not limited to DNF) or leave it as it is.

What to Do Now?

If you need the AFA-bits format immediately, I suggest manually transforming all transition formulae into DNF. Mentioned automaton ltl_afa/created_ltl/LTLf-specific/Response/N360.mata loads perfectly after this transformation.

[jn1z]

Thank you for tracking this down! I doubt I'll be manually transforming all of the transition formulae of Automata-Bench, but this is useful.

"Is It Really a Bug?"

Er... yes! :-)

Either:

1. This is not the "official automata format", in which case the Verifit Automata-Bench library, https://github.com/VeriFIT/automata-bench, has a bug (or several, depending on your definition).
2. The Mata library is not parsing the "official automata format" correctly.

However, in either case, Mata shouldn't be seg-faulting on these files. A user isn't going to be able to figure out the necessary format change (converting to DNF) from the seen behavior.