Skip to content

Adding LTL PropertyMonitor generation and the notion of FaultDomain

Niklas Krafczyk requested to merge feature-ltlMonitor-generation into master

This introduces functionality to read a file with a fault domain specification and a file with an LTL formula, create a propositional abstraction of the LTL formula, invoke the ltl2mon tool from ltl3tools, parse its output and translate that back to a monitor that can execute that monitor for concrete inputs.

Merge request reports