{"action":"opened","issue":{"url":"https://api.github.com/repos/reactive-systems/syfco/issues/15","repository_url":"https://api.github.com/repos/reactive-systems/syfco","labels_url":"https://api.github.com/repos/reactive-systems/syfco/issues/15/labels{/name}","comments_url":"https://api.github.com/repos/reactive-systems/syfco/issues/15/comments","events_url":"https://api.github.com/repos/reactive-systems/syfco/issues/15/events","html_url":"https://github.com/reactive-systems/syfco/issues/15","id":154849699,"number":15,"title":"TLSF initial condition quantification","user":{"login":"johnyf","id":3135273,"avatar_url":"https://avatars.githubusercontent.com/u/3135273?v=3","gravatar_id":"","url":"https://api.github.com/users/johnyf","html_url":"https://github.com/johnyf","followers_url":"https://api.github.com/users/johnyf/followers","following_url":"https://api.github.com/users/johnyf/following{/other_user}","gists_url":"https://api.github.com/users/johnyf/gists{/gist_id}","starred_url":"https://api.github.com/users/johnyf/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/johnyf/subscriptions","organizations_url":"https://api.github.com/users/johnyf/orgs","repos_url":"https://api.github.com/users/johnyf/repos","events_url":"https://api.github.com/users/johnyf/events{/privacy}","received_events_url":"https://api.github.com/users/johnyf/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":0,"created_at":"2016-05-14T11:52:49Z","updated_at":"2016-05-14T11:52:49Z","closed_at":null,"body":"#14 concerns the correspondence between TLSF and AIGER initial conditions. If a unique 0 initial state is defined in TLSF, then that fixes the AIGER initial state, and there is no question of quantification.\r\n\r\nIf not, i.e., multiple initial conditions are admissible in TLSF, then it seems that universal quantification is to be understood for these initial conditions. In other words, that the winning states should include all initial states. (In `slugs`, this is called [\"robotics semantics\"](https://github.com/VerifiableRobotics/slugs/blob/05bc151f60dff8af7fe1540673a60901b69532a0/src/extensionRoboticsSemantics.hpp#L31). In `gr1c` there is an option to choose the initial quantification, see [\"Interpretations of initial conditions\"](http://slivingston.github.io/gr1c/md_spc_format.html).)\r\n\r\nIf alternating quantification is used (`ALL_ENV_EXIST_SYS_INIT` in `gr1c`, default behavior of `slugs`), then there should be a way for the synthesizer to express within the AIGER circuit what initial values of the `Xc` latches it chooses.\r\n\r\nIn more detail, there are two options for alternation, `\\forall Xu: \\exists Xc` and `\\exists Xc: \\forall Xu`:\r\n\r\n- `\\exists Xc: \\forall Xu`: then the synthesizer would have to pick a fixed initial value for the `Xc` latches that works for all possible `Xu`. I think that there *is* a way for the synthesizer to incorporate such an initial condition in AIGER: under the assumption that all latches are initially 0, negate latches in the circuit, in order to obtain a negative initial condition for that variable.\r\n    \r\n    For example, variable `x` would no more be the latch `a`, but the signal `! a` for a latch `a`. The problem with this approach is that the latch names can no more be those of variables. Nonetheless, this can be rectified by a suitable definition of outputs as negated latches, accordingly.\r\n\r\n- `\\forall Xu: \\exists Xc`: then the synthesizer would produce a function that takes the initial condition `Xu` (some latches) and produces the initial condition `Xc = f(Xu)`. This `f` would itself be a combinational circuit involving latches only, but defining it seems to be outside the scope of AIGER.\r\n\r\nSo, in TLSF, will a single initial state, or multiple universally quantified states, or multiple `\\exists \\forall` states be given?"}}