Fix boolean over path ops in JaniParser

[vivoeiva]

Currently JaniParser emits BooleanStateFormula whenever it reaches a boolean operator over some other operator(s). This change it to actual check if one of the op's underneath is a path operator and emits BooleanPathFormula / BooleanStateFormula depending on that check.

Tests expanded to check for new behavior. The embedded die.jani also passes through the actual MC and emits plausible results.

[Copilot]

🔵 Needs a closer look

Add tests combining one state operand with one path operand in both orders.

Pull request overview

Updates JaniParser to correctly distinguish state and path boolean formulas.

Changes:

• Added path-aware boolean formula construction.
• Expanded parser tests for boolean formula classifications.

File summaries

File	Summary
src/test/storm/parser/JaniParserTest.cpp	Adds coverage for path/state boolean formulas.
src/storm-parsers/parser/JaniParser.cpp	Selects formula types based on path operands; mixed state/path operand coverage remains needed.

Review details

Suppressed comments (1)

src/storm-parsers/parser/JaniParser.cpp:337

• This branch is intended to handle the case where only one operand is a path formula, but every new binary test uses two path operands. A regression from || to && would therefore still pass the conjunction, disjunction, and implication tests; add a JANI property with one state operand and one path operand (ideally in both operand orders) and assert that it produces a BinaryBooleanPathFormula.

    if (left->isPathFormula() || right->isPathFormula()) {

• Files reviewed: 2/2 changed files
• Comments generated: 0
• Review effort level: Lite

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[volkm]

The code looks good to me.

@tquatmann Are the any conceptual issues with this change I might have overlooked?