search

VerifiableRobotics / LTLMoPWeb3D

A website for Cornell's Autonomous Systems Lab to essentially have LTLMoP available in 3D and online
https://ltlmop.herokuapp.com/
Other
3 stars 1 forks source link

Separate saveSpec functionality from createSpec/compileSpec #10

Closed agilgur5 closed 8 years ago

agilgur5 commented 9 years ago

So that when you compile, you don't have to download the spec. And so that the endpoint for saving is independent of spec creation.

This was attempted earlier but there was an error with Flask when I did this

agilgur5 commented 9 years ago

Figured out a way to do this effectively. saveSpec can just upload the spec to the server, and, upon success, just open that file on the server (using a hidden form submit). compileSpec will then just do the upload prior to compiling. Alternatively, saveSpec can be implemented entirely in the front end without too much effort.

agilgur5 commented 9 years ago

Really wanna do this entirely on front end... @jimjing how is the RegionMapping produced if the spec has not been compiled yet?

agilgur5 commented 8 years ago

Done. @jimjing still looking to do it front end only

agilgur5 commented 8 years ago

RegionMapping is produced after compilation (since it's literally a mapping from .regions to _decomposed.regions), so this needs to be passed back as well to the front end (proj.RegionMapping?), it's just a dictionary.