[Bug 436033] New: Review Request: mona - a solver for the WS1S and WS2S logics

[Red Hat Bugzilla]

Please do not reply directly to this email. All additional
comments should be made in the comments box of this bug report.

https://bugzilla.redhat.com/show_bug.cgi?id=436033

Summary: Review Request: mona - a solver for the WS1S and WS2S
                    logics
           Product: Fedora
           Version: rawhide
          Platform: All
        OS/Version: Linux
            Status: NEW
          Severity: medium
          Priority: medium
         Component: Package Review
        AssignedTo: [e-mail]
        ReportedBy: [e-mail]
         QAContact: [e-mail]
                CC: [e-mail],[e-mail]

Spec URL: http://jjames.fedorapeople.org/mona/mona.spec
SRPM URL: http://jjames.fedorapeople.org/mona/mona-1.4r9-1.src.rpm
Description: MONA is a tool that translates formulas in the logics WS1S and WS2S into finite-state automata represented by BDDs.  The formulas may express search patterns, temporal properties of reactive systems, parse tree constraints, etc.  MONA also analyzes the automaton resulting from the compilation, and determines whether the formula is valid and, if the formula is not valid, generates a counterexample.

Upstream produces a single binary.  I have patched the build system to split out the guts as libraries.  I did this because I am aware of multiple other projects that ship the MONA sources with their projects specifically so they can get access to those guts (e.g., the formal proof assistant PVS).  I am working with upstream (the differences between 1.4-8 and 1.4-9 are largely my doing), and will try to get this change incorporated as well.