Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib @ de84f40d

Name Size
  GMLMIP-0.1
ALCFormula.ml 54.2 KB
ALCFormula.mli 3.3 KB
ALCGraph.ml 15.1 KB
ALCGraph.mli 160 Bytes
ALCMisc.ml 31.5 KB
CoAlgFormula.ml 66.9 KB
CoAlgFormula.mli 6.02 KB
CoAlgLogicUtils.ml 3.58 KB
CoAlgLogicUtils.mli 285 Bytes
CoAlgLogics.ml 17.7 KB
CoAlgLogics.mli 204 Bytes
CoAlgMisc.ml 45.8 KB
CoAlgMisc.mli 12.3 KB
CoAlgReasoner.ml 33.3 KB
CoAlgReasoner.mli 794 Bytes
CoolUtils.ml 1.91 KB
CoolUtils.mli 1.08 KB
FunctorParsing.ml 6.72 KB
FunctorParsing.mli 576 Bytes
HashConsing.ml 8.64 KB
HashConsing.mli 699 Bytes
MiscSolver.ml 13.1 KB
MiscSolver.mli 1.29 KB
altGenlex.ml 9.45 KB
altGenlex.mli 416 Bytes
genAndComp.ml 68.2 KB
glpk.ml 6.94 KB
glpk.mli 7.13 KB
glpk_stub.c 10.7 KB
gmlmip.ml 406 Bytes
gmlmip.mli 597 Bytes
gmlmip_stub.c 3.47 KB
minisat.ml 1.06 KB
minisat.mli 455 Bytes
minisat_stub.c 3.33 KB

Latest revisions

# Date Author Comment
de84f40d 04/08/2016 08:08 PM Christoph Egger

Mark deferrals bold in graphviz export

0a6a3df5 04/08/2016 02:29 AM Christoph Egger

Fix inclusion condition for A_x

2fba43c0 04/08/2016 02:28 AM Christoph Egger

Make Sat children actually propagate their state to the parents

46cd6856 04/08/2016 02:26 AM Christoph Egger

Preliminarily mark States with no childs Sat in propagateSatMu

Should actually happen when the State changes from `Expandable` to
`Open` and trigger the propagateSatMu but for now just do it in
propagateSatMu so we can observe the algorithm working.

07a36b24 04/07/2016 05:35 PM Christoph Egger

Reorganize code, start from Sat nodes as well

Not only finishing cycles but also plain sat nodes may cause a node to
be satisfiable

67b07e54 04/07/2016 04:16 AM Christoph Egger

Restrict finishing nodes used as startingpoint

Only finishing nodes with enough Open / Sat children are to be
considered as startingpoints

Also accept already Satisfiable nodes when finding paths

1d5d9896 04/07/2016 02:38 AM Christoph Egger

Call new propagateSatMu instead of old propagateSat

6bbde09c 04/07/2016 02:37 AM Christoph Egger

preliminary propafateSat for μ-Calculus

This still produces wrong results: It assumes every node with empty
focus to be sat.

6d64bc5a 04/07/2016 02:35 AM Christoph Egger

whitespace cleanup

50df1dc2 04/07/2016 02:34 AM Christoph Egger

Add function to determin size of Core / State set

View revisions

Also available in: Atom