{"action":"created","issue":{"url":"https://api.github.com/repos/adl/hoaf/issues/38","labels_url":"https://api.github.com/repos/adl/hoaf/issues/38/labels{/name}","comments_url":"https://api.github.com/repos/adl/hoaf/issues/38/comments","events_url":"https://api.github.com/repos/adl/hoaf/issues/38/events","html_url":"https://github.com/adl/hoaf/issues/38","id":59341418,"number":38,"title":"multiple transitions with same source/label/destination, but different acceptance ","user":{"login":"adl","id":822900,"avatar_url":"https://avatars.githubusercontent.com/u/822900?v=3","gravatar_id":"","url":"https://api.github.com/users/adl","html_url":"https://github.com/adl","followers_url":"https://api.github.com/users/adl/followers","following_url":"https://api.github.com/users/adl/following{/other_user}","gists_url":"https://api.github.com/users/adl/gists{/gist_id}","starred_url":"https://api.github.com/users/adl/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/adl/subscriptions","organizations_url":"https://api.github.com/users/adl/orgs","repos_url":"https://api.github.com/users/adl/repos","events_url":"https://api.github.com/users/adl/events{/privacy}","received_events_url":"https://api.github.com/users/adl/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/adl/hoaf/labels/bug","name":"bug","color":"fc2929"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2015-02-28T13:15:40Z","updated_at":"2015-03-05T23:49:02Z","closed_at":null,"body":"If we ignore alternation, the semantic we give for omega automata with transition-based acceptance assume that the set of transitions and the acceptance sets are subsets of `Q*B(AP)*Q` where `B(AP)` is the set of Boolean functions.  However our syntax allows automata that cannot easily fit into this constraint.\r\n\r\nConsider this:\r\n\r\n    /* ... */\r\n    Start: 0\r\n    AP: 1 \"a\"\r\n    Acceptance: 2 Inf(0) & Inf(1)\r\n    --BODY--\r\n    State: 0\r\n    [0] 0 {0}\r\n    [0] 0 {1}\r\n    --END--\r\n\r\nthis declare two transitions `(0)-a->(0)`, each of them in a different acceptance set.   But our semantics do not support distinguishing these transitions.  Of course we could interpret this situation as a single transition that belongs to both sets: indeed if one of these transitions appear infinitely often in a run, the other transition can be used infinitely often as well.  So this automaton is equivalent to the following:\r\n\r\n    /* ... */\r\n    Start: 0\r\n    AP: 1 \"a\"\r\n    Acceptance: 2 Inf(0) & Inf(1)\r\n    --BODY--\r\n    State: 0\r\n    [0] 0 {0 1}\r\n    --END--\r\n\r\n(Shameless plug: Spot's `autfilt --merge-transitions` will do this simplification if you need it.)\r\nHowever this reduction is only correct because we are using Inf acceptance.\r\nFor instance consider again the first automaton, but negating the acceptance condition:\r\n \r\n    /* ... */\r\n    Start: 0\r\n    AP: 1 \"a\"\r\n    Acceptance: 2 Fin(0) | Fin(1)\r\n    --BODY--\r\n    State: 0\r\n    [0] 0 {0}\r\n    [0] 0 {1}\r\n    --END--\r\n\r\nThe above non-deterministic automaton is accepting since we can decide to stop using one of the two transitions at some point.  We cannot consider the two transition as being a single transition that\r\nbelongs to both sets, otherwise the automaton would be non-accepting.  If fact, because the sets are Fin-accepting, we could declare the `(0)-a->(0)` transition in their intersection if we want to avoid duplicate transitions.\r\n\r\nUsing intersection of `Fin` sets, and union for `Inf` sets fail when the same set number is used both with `Fin` and `Inf`.   Consider for instance the same automaton with:\r\n\r\n    Acceptance: 2 (Fin(0)&Inf(1)) | (Inf(0)&Fin(1))    /* = Inf(0) xor Inf(1) */\r\n\r\nI believe we have to change the semantics to support duplicate transitions in different acceptance sets to ensure that they work for any automaton we can represent with HOAF.  \r\n\r\nHere are two ideas for a possible fix:\r\n\r\n- Change `Q*B(AP)*Q` to something like `Q*B(AP)*2^F*Q` where `F` is a set of /acceptance numbers/.  Then change the acceptance of a run to extract the set of acceptance numbers seen infinitely often and make sure this set is compatible with the acceptance formula.\r\n- Change `Q*B(AB)*Q` to something like `Q*B(AB)*N*Q` where N are just natural numbers to allow us to duplicate transitions, but are not used for any other purpose.  In this case `F` can remain a set of subsets of transitions.\r\n\r\nI like the second option better because it still makes it clear we think in terms of acceptance sets of transitions."},"comment":{"url":"https://api.github.com/repos/adl/hoaf/issues/comments/77478116","html_url":"https://github.com/adl/hoaf/issues/38#issuecomment-77478116","issue_url":"https://api.github.com/repos/adl/hoaf/issues/38","id":77478116,"user":{"login":"strejcek","id":6370586,"avatar_url":"https://avatars.githubusercontent.com/u/6370586?v=3","gravatar_id":"","url":"https://api.github.com/users/strejcek","html_url":"https://github.com/strejcek","followers_url":"https://api.github.com/users/strejcek/followers","following_url":"https://api.github.com/users/strejcek/following{/other_user}","gists_url":"https://api.github.com/users/strejcek/gists{/gist_id}","starred_url":"https://api.github.com/users/strejcek/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/strejcek/subscriptions","organizations_url":"https://api.github.com/users/strejcek/orgs","repos_url":"https://api.github.com/users/strejcek/repos","events_url":"https://api.github.com/users/strejcek/events{/privacy}","received_events_url":"https://api.github.com/users/strejcek/received_events","type":"User","site_admin":false},"created_at":"2015-03-05T23:49:02Z","updated_at":"2015-03-05T23:49:02Z","body":"Wow, very interesting bug indeed. (Nice catch.)\r\n\r\nI can see one more solution: we can replace the set of transitions, which is  a subset of  `Q*B(AP)*Q`, by a *multiset* of transitions, where each transition is an element of `Q*B(AP)*Q`.\r\nWith this solution, no other changes in the definitions are needed. Or not?\r\nI like it more than introducing artificial transition numberings by `Q*B(AP)*N*Q`.\r\n"}}