Project

General

Profile

Activity

From 03/23/2016 to 04/21/2016

04/19/2016

08:07 PM Revision 0debe698 (cool): Rewrap some code to fit into 90 chars width
Christoph Egger
08:07 PM Revision 6aa0e444 (cool): Only deallocate solver for unsat nodes
We want to still have the solver for naive unsat propagation Christoph Egger
06:34 PM Revision e0906550 (cool): Remove debug output
Christoph Egger
06:32 PM Revision 54c89878 (cool): Only remove solver after Unsat Propagation
Christoph Egger
10:30 AM Revision 9f1263ec (cool): Deallocate satsolver once core becomes `Open`
The satsolver is reatined and only updated with new clauses for every
state that is generated out of a core. Once the...
Christoph Egger

04/18/2016

07:09 PM Revision dce4e4aa (cool): Use proper number of open States when calculating frequency
Instead of some calculation based of finishing on normal Cores really
count proper Open States
Christoph Egger

04/14/2016

06:37 PM Revision 4f821479 (cool): substract number of finishing/Sat nodes when calculating propagation fr...
Christoph Egger
06:30 PM Revision 1c26e356 (cool): Remove nominal propagation for now
Christoph Egger
06:18 PM Revision 55dc0a64 (cool): Make number of waves between propagation depend on #openCores
Christoph Egger
05:53 PM Revision 61c5af02 (cool): Do propagation only after 100 iterations
Christoph Egger
05:44 PM Revision 07c71f1c (cool): Add comment
Christoph Egger
04:23 PM Revision 31229254 (cool): Do both sat and unsat propagation
Christoph Egger
04:13 PM Revision 9c174a95 (cool): Remove debug output from propagateSatMu
Christoph Egger

04/13/2016

11:43 PM Revision e4faff97 (cool): Do a final propagation round at the end
Christoph Egger
10:18 PM Revision 012c092c (cool): Obvious simplification
Christoph Egger
10:07 PM Revision 8ab82480 (cool): Fix typo in propagateUnsatMu function name
Christoph Egger
09:54 PM Revision e1489b0d (cool): Expandable states are always acceptable Finishing states for Unsat prop...
Christoph Egger
09:33 PM Revision 86948fae (cool): Switch to only unsat propagation for testing
Christoph Egger
09:31 PM Revision c4142480 (cool): If root is Sat, formula is unconditionally Sat
Christoph Egger
03:04 AM Revision 5956a56d (cool): First implementation of propagateUnsat
Christoph Egger
02:35 AM Revision 066ed7b8 (cool): Fix syntax error introduced in last commit
Christoph Egger
02:20 AM Revision 1b17ef3c (cool): Fix bug in FL calculation and refocusing after states
Christoph Egger

04/12/2016

03:51 PM Revision 435390a8 (cool): Some adjustment to AB / EB
Christoph Egger
03:02 PM Revision 22fef65c (cool): Fixup for last commit
Christoph Egger
02:54 PM Revision 97d73a78 (cool): Fix A ( φ U ψ ) and E ( φ U ψ ) translation
Christoph Egger

04/11/2016

01:46 PM Revision 2f126161 (cool): Add some comments to propagateSatMu
Christoph Egger
02:43 AM Revision 4942adb7 (cool): Add graph subcommand to coalg
Christoph Egger

04/10/2016

01:29 AM Revision 3c05e89f (cool): Allow finishing cycles depending on only Sat states
Christoph Egger
12:13 AM Revision e30caa42 (cool): Implement {A,E}( .. {R,B} ..) CTL formulas
Christoph Egger
11:23 PM Revision 92102c11 (cool): Don't assume Open means Sat when finished
Assumption doesn't hold true currently Christoph Egger
11:12 PM Revision 3f073372 (cool): Treat Sat states like finishing states
With Sat states only treated like other states in the second fixpoint
iteration, the outer fixpoint was not ncessaril...
Christoph Egger

04/09/2016

10:15 PM Revision 080482ac (cool): Consider expanable Cores (but not states)
Acceptance test for cores is ∃ which is safe to use when non or only
some child states are created tus far
Christoph Egger
10:15 PM Revision 9fb4b019 (cool): Turn inner fixpoint inside-out
Christoph Egger
03:18 AM Revision f20718d2 (cool): Add header for function used in previous commit
Christoph Egger
03:17 AM Revision fe81b988 (cool): Make real empty set for deferral (not including True)
Christoph Egger
03:17 AM Revision ef0e7121 (cool): Actually use refocused deferral in modal step
Christoph Egger

04/08/2016

08:09 PM Revision 215ad4d7 (cool): Mark `True` only node as Sat
Christoph Egger
08:08 PM Revision 1e781c93 (cool): For now, don't consider Expandable states
Christoph Egger
08:08 PM Revision de84f40d (cool): Mark deferrals bold in graphviz export
Christoph Egger
02:29 AM Revision 0a6a3df5 (cool): Fix inclusion condition for A_x
Christoph Egger
02:28 AM Revision 2fba43c0 (cool): Make Sat children actually propagate their state to the parents
Christoph Egger
02:26 AM Revision 46cd6856 (cool): 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 ...
Christoph Egger

04/07/2016

05:35 PM Revision 07a36b24 (cool): Reorganize code, start from Sat nodes as well
Not only finishing cycles but also plain sat nodes may cause a node to
be satisfiable
Christoph Egger
04:16 AM Revision 67b07e54 (cool): Restrict finishing nodes used as startingpoint
Only finishing nodes with enough Open / Sat children are to be
considered as startingpoints
Also accept already Sati...
Christoph Egger
02:38 AM Revision 1d5d9896 (cool): Call new propagateSatMu instead of old propagateSat
Christoph Egger
02:37 AM Revision 6bbde09c (cool): preliminary propafateSat for μ-Calculus
This still produces wrong results: It assumes every node with empty
focus to be sat.
Christoph Egger
02:35 AM Revision 6d64bc5a (cool): whitespace cleanup
Christoph Egger
02:34 AM Revision 50df1dc2 (cool): Add function to determin size of Core / State set
Christoph Egger

04/05/2016

04:57 PM Revision 7b21fbae (cool): Some more comments
Christoph Egger
02:56 AM Revision b9a8d969 (cool): Space normalization
Christoph Egger
02:55 AM Revision f4498ed1 (cool): Add documentation on dependencies
Christoph Egger
 

Also available in: Atom