{"action":"created","issue":{"url":"https://api.github.com/repos/JuliaReach/Reachability.jl/issues/275","repository_url":"https://api.github.com/repos/JuliaReach/Reachability.jl","labels_url":"https://api.github.com/repos/JuliaReach/Reachability.jl/issues/275/labels{/name}","comments_url":"https://api.github.com/repos/JuliaReach/Reachability.jl/issues/275/comments","events_url":"https://api.github.com/repos/JuliaReach/Reachability.jl/issues/275/events","html_url":"https://github.com/JuliaReach/Reachability.jl/issues/275","id":367161991,"node_id":"MDU6SXNzdWUzNjcxNjE5OTE=","number":275,"title":"Low-dimensional discrete post operator","user":{"login":"schillic","id":9656686,"node_id":"MDQ6VXNlcjk2NTY2ODY=","avatar_url":"https://avatars2.githubusercontent.com/u/9656686?v=4","gravatar_id":"","url":"https://api.github.com/users/schillic","html_url":"https://github.com/schillic","followers_url":"https://api.github.com/users/schillic/followers","following_url":"https://api.github.com/users/schillic/following{/other_user}","gists_url":"https://api.github.com/users/schillic/gists{/gist_id}","starred_url":"https://api.github.com/users/schillic/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/schillic/subscriptions","organizations_url":"https://api.github.com/users/schillic/orgs","repos_url":"https://api.github.com/users/schillic/repos","events_url":"https://api.github.com/users/schillic/events{/privacy}","received_events_url":"https://api.github.com/users/schillic/received_events","type":"User","site_admin":false},"labels":[{"id":731810443,"node_id":"MDU6TGFiZWw3MzE4MTA0NDM=","url":"https://api.github.com/repos/JuliaReach/Reachability.jl/labels/feature","name":"feature","color":"f0ad4e","default":false}],"state":"open","locked":false,"assignee":{"login":"schillic","id":9656686,"node_id":"MDQ6VXNlcjk2NTY2ODY=","avatar_url":"https://avatars2.githubusercontent.com/u/9656686?v=4","gravatar_id":"","url":"https://api.github.com/users/schillic","html_url":"https://github.com/schillic","followers_url":"https://api.github.com/users/schillic/followers","following_url":"https://api.github.com/users/schillic/following{/other_user}","gists_url":"https://api.github.com/users/schillic/gists{/gist_id}","starred_url":"https://api.github.com/users/schillic/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/schillic/subscriptions","organizations_url":"https://api.github.com/users/schillic/orgs","repos_url":"https://api.github.com/users/schillic/repos","events_url":"https://api.github.com/users/schillic/events{/privacy}","received_events_url":"https://api.github.com/users/schillic/received_events","type":"User","site_admin":false},"assignees":[{"login":"schillic","id":9656686,"node_id":"MDQ6VXNlcjk2NTY2ODY=","avatar_url":"https://avatars2.githubusercontent.com/u/9656686?v=4","gravatar_id":"","url":"https://api.github.com/users/schillic","html_url":"https://github.com/schillic","followers_url":"https://api.github.com/users/schillic/followers","following_url":"https://api.github.com/users/schillic/following{/other_user}","gists_url":"https://api.github.com/users/schillic/gists{/gist_id}","starred_url":"https://api.github.com/users/schillic/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/schillic/subscriptions","organizations_url":"https://api.github.com/users/schillic/orgs","repos_url":"https://api.github.com/users/schillic/repos","events_url":"https://api.github.com/users/schillic/events{/privacy}","received_events_url":"https://api.github.com/users/schillic/received_events","type":"User","site_admin":false}],"milestone":null,"comments":0,"created_at":"2018-10-05T11:01:17Z","updated_at":"2018-10-10T13:16:02Z","closed_at":null,"author_association":"MEMBER","body":"Terminology: An *embedded set* is a high-dimensional set that is universal in some dimensions. Let `U(m)` be the `m`-dimensional universal set. Then I am talking about a set `U(k) × L × U(l)` with `L` being a low-dimensional set. For example, an interval embedded in 2D is a thick vertical or horizontal line, depending on whether it is defined for the dimension x1 or x2.\r\n\r\nTo take the intersection of two embedded sets, it suffices to take the intersection for the non-universal dimensions and (if not empty) embed again in high dimensions.\r\n\r\n### Name for embedded sets\r\n\r\nWhat is a good name?\r\n\r\n### Interface for embedded sets\r\nI think we can assume that the input system is given in full dimensions. Thus we need some way to detect embedded sets in the first place.\r\n\r\nAfter detection, we need to store this information. We can either create a new system (which requires to minimally change the current interface) or have some additional data structure (sounds complicated).\r\nFor instance, we could have a wrapper `Embedding(L::LazySet{N}, n::Int, i0::Int) <: LazySet{N}` in `LazySets` which takes a low-dimensional set `L` and acts like a high-dimensional set in `n` dimensions, where `i0` is the first index where the set is not universal (i.e., the represented set is `U(i0-1) × L × U(n-(i0+dim(L)-1))`)."},"comment":{"url":"https://api.github.com/repos/JuliaReach/Reachability.jl/issues/comments/428566980","html_url":"https://github.com/JuliaReach/Reachability.jl/issues/275#issuecomment-428566980","issue_url":"https://api.github.com/repos/JuliaReach/Reachability.jl/issues/275","id":428566980,"node_id":"MDEyOklzc3VlQ29tbWVudDQyODU2Njk4MA==","user":{"login":"schillic","id":9656686,"node_id":"MDQ6VXNlcjk2NTY2ODY=","avatar_url":"https://avatars2.githubusercontent.com/u/9656686?v=4","gravatar_id":"","url":"https://api.github.com/users/schillic","html_url":"https://github.com/schillic","followers_url":"https://api.github.com/users/schillic/followers","following_url":"https://api.github.com/users/schillic/following{/other_user}","gists_url":"https://api.github.com/users/schillic/gists{/gist_id}","starred_url":"https://api.github.com/users/schillic/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/schillic/subscriptions","organizations_url":"https://api.github.com/users/schillic/orgs","repos_url":"https://api.github.com/users/schillic/repos","events_url":"https://api.github.com/users/schillic/events{/privacy}","received_events_url":"https://api.github.com/users/schillic/received_events","type":"User","site_admin":false},"created_at":"2018-10-10T13:16:02Z","updated_at":"2018-10-10T13:16:02Z","author_association":"MEMBER","body":"While I still think the above is an interesting approach, for now I will try a straightforward one: For your current location, find *all* dimensions that are relevant for the guards, and then do the continuous post only in those dimensions (for now: use 1D blocks). Then, for each transition, take a projection of the source invariant and guard in those dimensions. Then we have to compute those reach sets where the invariant intersects in high dimensions again (this will be the most complicated part). We should repeat the invariant intersection to see if we missed something in the first round, but this could be optional. Finally, we apply the assignment and take the intersection with the target invariant, which happens again in high dimensions."}}
{"actor":{"display_login":"schillic"}}