Skip to content

[WIP] BA to slim BA - #31

Open
psimovec wants to merge 26 commits into
mklokocka:masterfrom
psimovec:ba2slim
Open

[WIP] BA to slim BA#31
psimovec wants to merge 26 commits into
mklokocka:masterfrom
psimovec:ba2slim

Conversation

@psimovec

@psimovec psimovec commented Sep 19, 2020

Copy link
Copy Markdown

The algorithm for slim automata construction is described in section 3.2 here: https://link.springer.com/content/pdf/10.1007%2F978-3-030-45190-5_17.pdf (seminator --slim --strong --via-tba)

Latest jupyter notebook demo: https://github.com/psimovec/seminator/blob/ba2slim/notebooks/slim_ba.ipynb

Step 1 ✔️
extract BP algorithm from bp_twa
relevant jupyter notebook

Step 2 ✔️ ⚠️
add "slim" transitions
⚠️ done, but breaks bp_twa class
relevant jupyter notebook
fix this in follow-up commits ✔️

Step 3 ✔️
Change --slim from being desired output to classic argument..
add --bp argument to display BP automaton
relevant notebook

Step 4 : ✔️
Fix bug in construction that @xblahoud pointed out here (bug), thanks!
fixed: notebook with fix

Step 5: ✔️
add tests for slim automata

Step 6: ✔️ ❓
"done", the algorithm looks that works, and the tests pass. But it's correctness isn't proved or anything like that.

Step 7: ✔️
BP and slim edges distinguished by belonging to a different accepting state set ✔️
better visualization of slim automata - a different color for bp/slim edges/states ✔️

Step 8: TODO, or not TODO, that is the question
move BP algorithm from slim constructor to bp_twa method to get rid of unnecessary changes of private properties to public

alternative - just rename slim class to some kind of breakpoint automaton, and bp_twa would use this...

TODO:
pure BP algo might not be working
use better names of variables
create tests of language equivalence on random generated automata
on input/slim/ weak slim
random generated could have TGBAs.. On test failure it could give a hint if something is needed to change..
generalize for TGBA

If slim.test fails, we can check output of --grind if it failed on LTLs where the ltl or it's negation generates TGBA with anything else than 1 accepting set
#!/bin/zsh
while read -r line; do echo $line;ltl2tgba $line|grep "Acceptance: [^1]";ltl2tgba --negate $line|grep "Acceptance: [^1]"; echo ""; done < grind.ltl

@psimovec psimovec changed the title [WIP] BA to slim BA [RFR] BA to slim BA Jul 7, 2021
@psimovec psimovec changed the title [RFR] BA to slim BA [WIP] BA to slim BA Jul 7, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants