hansjava

 Loading...
Author  Commit  Message  Date  Builds 

Adds explicit divergence and contribution documentation



Port recent changes to Haskell



Adds shortest path extraction



Adds small optimization.



Fixes bug in finding winning cycle: suppose that the function to determine a winning cycle is found always returns that a winning cycle is found but every vertex is connected to a dead end, then the algorithm is still correct since the dead end is prioritized over winning cycles for odd vertices and we already saw that for even vertices there is no occurrence of losing cycles and hence the return value seems correct.



Example finally passes. Current TODOs: extraction correctness proof, shortest path, code clean up, extension documentation



Simplified strategy implementation. Does not work correctly in bbsim_02.txt



This solution is too complex (and does not work); it tries to solve two problems at the same time (shortest path & cycle detection). Code will soon be replaced by factoring out solutions and composing them instead.



Algorithm works in base cases, but regresses for cycles



Initial implementation for new strategy extraction (not tested)



WIP



WIP



Adds test of intended duality property of Buchi game



Adds documentation to solveBuchiGame



Adds Buchi objective parameter to solver



Reverts change. Bad assumption: W_Odd is not complement of W_Even!



Synchronizes Haskell implementation to Frege.



Fixes pertinent issue (see email)



Partial fix of problem



Again buggy commit to discover bug (forgot to synchronize part of Haskell to Frege)



Inversion of buchi game solver (buggy!)



Fixes table scroll bar updating



Typo in Log value



Adds examples and further refactors source code to enable tracing attractorSets. Ports changes from Frege to Haskell. Verified tests: still failing.



Updates deployment documentation



Adds Buchi game stepper



Ports changes to Frege



Adds logging messages during solveBuchiGame (verified that it does not regress tests)



Removes BulychevGame, ParityGame and SimulationGame. Decreases number of source files, merging GameGraph, GameUtil and Player.



Reverts Buchi game solver, fixed mismatch between Frege and Haskell code (!)



Works around compiler bug, Buchi solver is not correctly adapted from original source



Frege fails to compile higherorder type. Tests are inadequate. (WIP, does not compile)



Updates Buchi solver to maintain trace of immediate results



Adds Buchi game solution dialog



Cleans up source. Verified that old Set implementation did not alter test results.



WIP



Updates README to include additional classpath and deployment instructions



Fixes spelling error in message log, adds special highight for current chall**e**nge.



Fix the game edges for the branching bisimulation game graph.
There were two issues here:
* Mimicking a tautransition by doing nothing was always rewarded, which is only correct in the branching bisimulation case, and not the divergencepreserving branching bisimulation case.
* Mimicking an astep with a tautransition was rewarded with a tick in the branchingbisimulation case, which is also incorrect.
I have manually traced the game graph now, and determâ€¦



For the failing test case, also check divergence preserving branching bisimulation.



Add failing test for branching bisimulation, see emails



Fix typos



Backports changes from Frege to Haskell, fixes bisimulation.



Adds game outcome. Adds explicit outcome message. (See email Tim)



Uncomments execution of old strategy if new strategy does not exists, fixes minor UI bug, relayouts data files.



Ports refined strategy extraction algorithm to Frege



Fixes minor UI bugs



Updates refined extraction algorithm



Adds initial implementation for marked edge set



Updates README and refactors Buchi game solver in anticipation of extraction algorithm



Ports Haskell changes and modifies visualizer to show example as in slides, implements bisimulation games



Fixes branching bisimulation and adds tests



Initial implementation of Java visualization and Frege port



045a56d
M

Merge branch 'hanslist' into hans



Fixes wrong set of winning vertices



Fixes implementation of ASet



Updates test w.r.t. label Int



Updates test w.r.t. label Int



Changes implementation of ASet to lists



Adds test cases, LTS labels by index



Initial interactive version for BisimulationGame



Adds bisimulation test



Syntax cleanup and uses abstract data type: ASet instead of Data.Set



Extracted Data.Set from GameGraph, to ease implementation based on lists.



Reproduced README instructions



HLinted, created cabal package with test suite, readme and licence

