{"action":"closed","issue":{"url":"https://api.github.com/repos/lgwagner/SpeAR/issues/37","repository_url":"https://api.github.com/repos/lgwagner/SpeAR","labels_url":"https://api.github.com/repos/lgwagner/SpeAR/issues/37/labels{/name}","comments_url":"https://api.github.com/repos/lgwagner/SpeAR/issues/37/comments","events_url":"https://api.github.com/repos/lgwagner/SpeAR/issues/37/events","html_url":"https://github.com/lgwagner/SpeAR/issues/37","id":176661209,"number":37,"title":"Feature request: Realizability analysis","user":{"login":"jendavis","id":15248196,"avatar_url":"https://avatars.githubusercontent.com/u/15248196?v=3","gravatar_id":"","url":"https://api.github.com/users/jendavis","html_url":"https://github.com/jendavis","followers_url":"https://api.github.com/users/jendavis/followers","following_url":"https://api.github.com/users/jendavis/following{/other_user}","gists_url":"https://api.github.com/users/jendavis/gists{/gist_id}","starred_url":"https://api.github.com/users/jendavis/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jendavis/subscriptions","organizations_url":"https://api.github.com/users/jendavis/orgs","repos_url":"https://api.github.com/users/jendavis/repos","events_url":"https://api.github.com/users/jendavis/events{/privacy}","received_events_url":"https://api.github.com/users/jendavis/received_events","type":"User","site_admin":false},"labels":[{"id":120290837,"url":"https://api.github.com/repos/lgwagner/SpeAR/labels/enhancement","name":"enhancement","color":"84b6eb","default":true}],"state":"closed","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":2,"created_at":"2016-09-13T14:47:24Z","updated_at":"2016-12-08T19:36:00Z","closed_at":"2016-12-08T19:36:00Z","body":"When requirements conflict some of the time but not all of the time, the requirements set will pass the consistency check in SpeAR. However, \"occasionally conflicting\" requirements implicitly constrain the input variables, which is not good and surprises the user. See the example below where requirements r1 and r2 conflict when the input a is equal to 3. Hence I can prove a property that a is never equal to 3, even though I have no such assumptions on the input a. Typically this implicit constraint on the input would be unbeknownst to the user. \n\nRealizability analysis is supported by AGREE and catches this kind of problem, providing a counterexample. I request that realizability analysis be added in the next major version of SpeAR. \n\n---\n\nSpecification test\n\nInputs:\na : int\n\nOutputs:\nb : int\n\nRequirements:\nr1: a==3 implies b==2\nr2: a==3 implies b==3\n\nProperties:\nbad_prop: not (a==3)\n"}}
{"actor":{"display_login":"lgwagner"}}