History | View | Annotate | Download (71.5 KB)

Don't hardcode check for aconjunctive formulas

Previously, cool would simply raise an exception if the formula wasnot aconjunctive. This was done to ease testing of the new reasoneralgorithm.

Now, the reasoner decides whether the formula is aconjunctive or not...

Add check for aconjunctive formulas

Add UTF-8 "Micro Sign" as syntax for 'mu'

This is easier to type with a standard compose key as opposed as thearguably more correct "Greek Small Letter Mu".

Add vim modeline to all OCaml files

Fix a few compiler warnings

Consider also other modal operators as valid guards

Revert to fresh variable names in convertToMu

Unify CTL variable name for more global caching

Some adjustment to AB / EB

Fixup for last commit

Fix A ( φ U ψ ) and E ( φ U ψ ) translation

Implement {A,E}( .. {R,B} ..) CTL formulas

Use custom variables for CTL -> μ

Makes morally same formulas actually the same. Removes the need torecalculate some States that have already been fully expanded but withdifferent variable names only (where this is possible)

Some seemingly missed patern-match cases

Add function to verify if deferral is still mentioned in formula

Whitespace cleanup

No tabs any more

Fix fixpoint-unfolding

Implement negation of Fixpoints also for HashConsed representation

Implement equality on (HC)μ/ν

Add function to substitute variables

add fallthrough cases (CTL constructors) for verify*

Fix guardednes check

Move verification of formula to separate step

Implement verify functions

implement nnf for μ-Calculus

allow arbitrary formulas in A(φ U ψ) and E(…)

previously only late parser steps were used so modalities were allowedbut not e.g. disjunctions. With this change all of theCTLComparisonBenchmarks formulas successfully parse

assume parens when parsing A(φ U ψ)

Example formulas from the benchmark seem to all have parens so assumethey are there

Add check for guardedness

Add prototypes for checker functions

We need to enforce some assumptions for μ-Calculus. Add (still empty)checker function and call them when importing the forumla

Add μ constructors to the formula iter

Generate instance of VAR instead of AP for bound variables

Add symbols bound in ν/μ expressions to table

Hand symbol table down the parser

Add pattern-matching for hcFormula where obvious

Add all obvious cases for hcFormula

Actually represent variable under μ/ν as string

so it's `MU of string * formula` again. The variable within the formulais still represented as `VAR s`

CTL is expected to be removed early on

Create pattern-matching cases for all CTL language elements and raise anerror if encountered. We are assuming that CTL is replaced by plainμ-Calculus early on

Add CTL and μ-Calculus Constructors to convert_post

Needed e.g. to implement the CTL → μ conversion

Add μ-constructors for hcFormula

CTL is assumed to be eliminated before the hash-consing step

Add gensym for CTL -> μ

Add function to convert CTL -> μ Calculus

Needs a #'gensym implementation for variable names still

Read/Write CTL

Add new datatypes for CTL

sizeFormula function for μ-Calculus

Read/Write μ-Calculus formulas

TODO: differentiate between APs and VARs on use. VAR is only used during declaration so far

Add μ / ν symbols to the lexer

Add New datatypes for μ-Calculus

Removed Negation Normal Form of Choice as Choice is Self-Dual

Added Identity Functor and Skeleton for Default Implication

Implement raw syntax for constant functors

Add more documentatoin about installing and hacking

Implement the REAL box of PML

Change AtMostProbable to LessProbableThan

The actual box of PML (in GMLMIP) is: less probable than. The Diamondis: At least Probable than.

So now you have ¬[p] C = <p> C.

Add ocaml part of PML rule application

Add formula constructors for PML

Remove unneeded variables

Fix equal_hcFormula_node for CL

Add syntax for PML

Improve OWL -> CoAlg conversion

Implement fuzzy formula conversion to K or GML

Separate cool into library and coalg frontend