{"action":"opened","issue":{"url":"https://api.github.com/repos/dreal/dreal/issues/96","labels_url":"https://api.github.com/repos/dreal/dreal/issues/96/labels{/name}","comments_url":"https://api.github.com/repos/dreal/dreal/issues/96/comments","events_url":"https://api.github.com/repos/dreal/dreal/issues/96/events","html_url":"https://github.com/dreal/dreal/issues/96","id":69590169,"number":96,"title":"Network Automata DRH syntax","user":{"login":"danbryce","id":968160,"avatar_url":"https://avatars.githubusercontent.com/u/968160?v=3","gravatar_id":"","url":"https://api.github.com/users/danbryce","html_url":"https://github.com/danbryce","followers_url":"https://api.github.com/users/danbryce/followers","following_url":"https://api.github.com/users/danbryce/following{/other_user}","gists_url":"https://api.github.com/users/danbryce/gists{/gist_id}","starred_url":"https://api.github.com/users/danbryce/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/danbryce/subscriptions","organizations_url":"https://api.github.com/users/danbryce/orgs","repos_url":"https://api.github.com/users/danbryce/repos","events_url":"https://api.github.com/users/danbryce/events{/privacy}","received_events_url":"https://api.github.com/users/danbryce/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":0,"created_at":"2015-04-20T13:44:10Z","updated_at":"2015-04-20T13:44:10Z","closed_at":null,"body":"We've developed a new syntax for drh files that includes some changes needed for networks of automata, but also some changes that are not specific to networks.  I've included an example below.  I'd like to integrate this syntax with dreal2 or dreal3, but am looking for input on how to proceed.  We can update the existing benchmarks, use a different parser, merge the parsers, etc. Any suggestions?\r\n\r\nCurrently, we have a branch on bitbucket that is built off of dreal2 and modifies dReach only.   \r\n\r\nHere is the example:\r\n\r\n\r\n[0, 100000] time;\r\n\r\n(component train;\r\n\t[0, 5000] x;\r\n\r\n\tlabel approach, exit;\r\n\r\n\t(mode far;\r\n\t\tinvt:\r\n\t\t\t(x >= 1000);\r\n\t\tflow:\r\n\t\t\td/dt[x] = -1;\r\n\t\tjump:\r\n\t\t\t(approach): (x = 1000) ==> @near (true);\r\n\t)\r\n\r\n\t(mode near;\r\n\t\tinvt:\r\n\t\t\t(x >= 0);\r\n\t\tflow:\r\n\t\t\td/dt[x] = -1;\r\n\t\tjump:\r\n\t\t\t(): (true) ==> @past (x' = 0);\r\n\t)\r\n\r\n\t(mode past;\r\n\t\tinvt:\r\n\t\t\t(x >= -100);\r\n\t\tflow:\r\n\t\t\td/dt[x] = -1;\r\n\t\tjump:\r\n\t\t\t(exit): (x = -100) ==> @near (x' = 4900);\r\n\t)\r\n)\r\n\r\n(component gate;\r\n\t[0, 90] y;\r\n\t\r\n\tlabel raise, lower;\r\n\t\r\n\t(mode open;\r\n\t\tinvt:\r\n\t\t\t(y <= 90);\r\n\t\tflow:\r\n\t\t\td/dt[y] = 0;\r\n\t\tjump:\r\n\t\t\t(raise): (true) ==> @open (y' = y);\r\n\t\t\t(lower): (true) ==> @movedown (y' = y);\r\n\t)\r\n\t\r\n\t(mode closed;\r\n\t\tinvt:\r\n\t\t\t(y = 0);\r\n\t\tflow:\r\n\t\t\td/dt[y] = 0;\r\n\t\tjump:\r\n\t\t\t(lower): (true) ==> @closed (y' = y);\r\n\t\t\t(raise): (true) ==> @moveup (y' = y);\r\n\t)\r\n\t\r\n\t(mode movedown;\r\n\t\tinvt:\r\n\t\t\t(y >= 0);\r\n\t\tflow:\r\n\t\t\td/dt[y] = -9;\r\n\t\tjump:\r\n\t\t\t(): (true) ==> @closed (y' = 0);\r\n\t\t\t(lower): (true) ==> @movedown (y' = y);\r\n\t\t\t(raise): (true) ==> @moveup (y' = y);\r\n\t)\r\n\t\r\n\t(mode moveup;\r\n\t\tinvt:\r\n\t\t\t(y >= 90);\r\n\t\tflow:\r\n\t\t\td/dt[y] = 9;\r\n\t\tjump:\r\n\t\t\t(): (true) ==> @open (y' = 90);\r\n\t\t\t(raise): (true) ==> @moveup (y' = y);\r\n\t\t\t(lower): (true) ==> @movedown (y' = y);\r\n\t)\r\n)\r\n\r\n(component controller;\r\n\t[0, 100000] z;\r\n\t\r\n\tlabel lower, raise, approach, exit;\r\n\t\r\n\t(mode doup;\r\n\t\tinvt:\r\n\t\t\t(z <= 5);\r\n\t\tflow:\r\n\t\t\td/dt[z] = 1;\r\n\t\tjump:\r\n\t\t\t(exit): (true) ==> @doup (z' = z);\r\n\t\t\t(raise): (true) ==> @idle (z' = z);\r\n\t\t\t(approach): (true) ==> @dodown (z' = z);\r\n\t)\r\n\t\r\n\t(mode idle;\r\n\t\tinvt:\r\n\t\tflow:\r\n\t\t\td/dt[z] = 1;\r\n\t\tjump:\r\n\t\t\t(exit): (true) ==> @doup (z' = 0);\r\n\t\t\t(approach): (true) ==> @dodown (z' = 0);\r\n\t)\r\n\t\r\n\t(mode dodown;\r\n\t\tinvt:\r\n\t\t\t(z <= 5);\r\n\t\tflow:\r\n\t\t\td/dt[z] = 1;\r\n\t\tjump:\r\n\t\t\t(approach): (true) ==> @dodown (z' = z);\r\n\t\t\t(exit): (true) ==> @doup (z' = z);\r\n\t\t\t(lower): (true) ==> @idle (z' = z);\r\n\t)\r\n)\r\n\r\nanalyze:\r\n\ttrain0 = train[[], @far (x=5000)];\r\n\tgate0 = gate[[], @open (y = 90)];\r\n\tcontroller0 = controller[[], @idle (z = 0)];\r\n\t(train0 || gate0 || controller0);\r\n\t\r\ngoal:\r\n\t(): (and (x <= 1000) (x >= 0) (y >= 0));\r\n//\t(): (and (x));"}}