Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgFormula.ml @ 946e8213

History | View | Annotate | Download (71.5 KB)

# Date Author Comment
b6653b96 04/06/2017 05:57 PM Hans-Peter Deifel

Don't hardcode check for aconjunctive formulas

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

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

fdda99d4 04/06/2017 05:56 PM Hans-Peter Deifel

Add check for aconjunctive formulas

5f1ec830 03/22/2017 04:54 PM Hans-Peter Deifel

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

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

a57eb439 03/21/2017 09:12 PM Hans-Peter Deifel

Add vim modeline to all OCaml files

e0e6eb62 03/16/2017 11:15 PM Hans-Peter Deifel

Fix a few compiler warnings

07402362 05/21/2016 03:50 AM Christoph Egger

Consider also other modal operators as valid guards

2a36974b 05/14/2016 10:16 PM Christoph Egger

Revert to fresh variable names in convertToMu

de13bc0f 05/10/2016 10:02 AM Christoph Egger

Unify CTL variable name for more global caching

435390a8 04/12/2016 03:51 PM Christoph Egger

Some adjustment to AB / EB

22fef65c 04/12/2016 03:02 PM Christoph Egger

Fixup for last commit

97d73a78 04/12/2016 02:54 PM Christoph Egger

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

e30caa42 04/11/2016 12:13 AM Christoph Egger

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

dcc8167f 02/22/2016 03:44 PM Christoph Egger

Use custom variables for CTL -> μ

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

fbffb079 02/16/2016 12:54 PM Christoph Egger

Some seemingly missed patern-match cases

5e7c8aa1 01/26/2016 04:29 PM Christoph Egger

Add function to verify if deferral is still mentioned in formula

c5c25acf 12/07/2015 04:53 PM Christoph Egger

Whitespace cleanup

No tabs any more

854e1338 12/07/2015 04:47 PM Christoph Egger

Fix fixpoint-unfolding

92feed46 12/01/2015 05:04 PM Christoph Egger

Implement negation of Fixpoints also for HashConsed representation

a7ae917b 12/01/2015 05:04 PM Christoph Egger

Implement equality on (HC)μ/ν

cc07e93d 12/01/2015 04:43 PM Christoph Egger

Add function to substitute variables

939f5bab 11/18/2015 02:37 PM Christoph Egger

add fallthrough cases (CTL constructors) for verify*

26cfb2dc 11/17/2015 04:14 PM Christoph Egger

Fix guardednes check

1484d8cb 11/17/2015 03:54 PM Christoph Egger

Move verification of formula to separate step

63710593 11/17/2015 03:53 PM Christoph Egger

Implement verify functions

ff4dc786 11/16/2015 11:29 PM Christoph Egger

implement nnf for μ-Calculus

993e31e1 11/10/2015 05:12 PM Christoph Egger

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

previously only late parser steps were used so modalities were allowed
but not e.g. disjunctions. With this change all of the
CTLComparisonBenchmarks formulas successfully parse

80bbb363 11/10/2015 04:30 PM Christoph Egger

assume parens when parsing A(φ U ψ)

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

a2cd9f2a 11/09/2015 08:03 PM Christoph Egger

Add check for guardedness

d2db7e40 11/09/2015 08:02 PM Christoph Egger

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

309b71a5 11/09/2015 08:01 PM Christoph Egger

Add μ constructors to the formula iter

c3e13ca6 11/09/2015 02:43 PM Christoph Egger

Generate instance of VAR instead of AP for bound variables

80aa0b2f 11/09/2015 02:43 PM Christoph Egger

Add symbols bound in ν/μ expressions to table

0b908205 11/09/2015 02:43 PM Christoph Egger

Hand symbol table down the parser

508e3c33 11/09/2015 02:43 PM Christoph Egger

Add pattern-matching for hcFormula where obvious

Add all obvious cases for hcFormula

d29d35f7 11/09/2015 02:43 PM Christoph Egger

Actually represent variable under μ/ν as string

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

8cac0897 11/09/2015 02:43 PM Christoph Egger

CTL is expected to be removed early on

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

7b944a64 11/09/2015 02:43 PM Christoph Egger

Add CTL and μ-Calculus Constructors to convert_post

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

87d5082f 11/09/2015 02:43 PM Christoph Egger

Add μ-constructors for hcFormula

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

17af2794 11/09/2015 02:43 PM Christoph Egger

Add gensym for CTL -> μ

c5105465 11/03/2015 04:52 PM Christoph Egger

Add function to convert CTL -> μ Calculus

Needs a #'gensym implementation for variable names still

0aa34675 10/30/2015 06:24 PM Christoph Egger

Read/Write CTL

b179a57f 10/30/2015 05:57 PM Christoph Egger

Add new datatypes for CTL

a5f60450 10/28/2015 05:16 PM Christoph Egger

sizeFormula function for μ-Calculus

8334c748 10/28/2015 05:14 PM Christoph Egger

Read/Write μ-Calculus formulas

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

b2f18312 10/28/2015 05:11 PM Christoph Egger

Add μ / ν symbols to the lexer

9a3b23cc 10/28/2015 05:10 PM Christoph Egger

Add New datatypes for μ-Calculus

d58bba0f 02/05/2015 07:02 AM Dirk Pattinson

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

19f5dad0 02/04/2015 05:02 AM Dirk Pattinson

Added Identity Functor and Skeleton for Default Implication

c49eea11 01/22/2015 06:58 PM Thorsten Wißmann

Implement raw syntax for constant functors

69a71d22 01/22/2015 01:15 PM Thorsten Wißmann

Add more documentatoin about installing and hacking

9bae2c4f 07/21/2014 01:49 PM Thorsten Wißmann

Implement the REAL box of PML

c855ba91 07/21/2014 11:34 AM Thorsten Wißmann

Change AtMostProbable to LessProbableThan

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

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

eda515b6 07/21/2014 11:05 AM Thorsten Wißmann

Add ocaml part of PML rule application

86b07be8 07/20/2014 11:05 AM Thorsten Wißmann

Add formula constructors for PML

4bfb63a1 07/20/2014 11:05 AM Thorsten Wißmann

Remove unneeded variables

bc6db513 07/20/2014 11:04 AM Thorsten Wißmann

Fix equal_hcFormula_node for CL

81435cc4 07/19/2014 06:38 PM Thorsten Wißmann

Add syntax for PML

e5422169 07/19/2014 06:36 PM Thorsten Wißmann

Add syntax for PML

ca99d0c6 05/06/2014 08:30 AM Thorsten Wißmann

Improve OWL -> CoAlg conversion

dbcce612 05/05/2014 01:16 PM Thorsten Wißmann

Implement fuzzy formula conversion to K or GML

7c4d2eb4 04/23/2014 11:21 AM Thorsten Wißmann

Separate cool into library and coalg frontend