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

Download Compiled Artifacts Asynchronously #54

Open agilgur5 opened 8 years ago

agilgur5 commented 8 years ago

On top of the log + ltl, the RegionMapping is needed for Workspace Decomposition. Are decomposed regions needed for counterstrategy...?

agilgur5 commented 8 years ago

Currently asynchronously reading in the Decomposed Regions. Will have to async read the Spec and Aut and should do that with LTL as well to speed up the compile request (so the server doesn't have to read in the whole file and then pass it back as text).

Optimized a lot of the server functionality as it no longer has to read and parse these files and pass back structured data. No need for 'createJSONForSpec' function in LTLMoP anymore or all the spec code that formats the project into a neat JSON dict.

agilgur5 commented 8 years ago

Async read of Aut + LTL complete. Removed LTL read from API. These blobs/files that are downloaded can just be cached and used for the Save buttons. Adding Spec + SMV would also obviate the need for the back end to create a zip file (which also takes a bit of time because disk access) and it could then be created on the front end entirely using something like https://github.com/Stuk/jszip.

This is different from #61 which is only for things that are NOT compiled artifacts, e.g. the currently being written spec and the regions file in the region editor.

agilgur5 commented 6 years ago

Not sure if this feature totally makes sense. It may make more sense to just have the API be totally stateless (which obviates the need for sessions, API keys, etc).

If it were stateless, there would basically only be two API methods -- compile and analyze, that both just accept files as their parameters. Compile would return the zip of the project (unless the other generated files can be derived in JS? e.g. LTL from Aut?) including the log and the front-end would unzip and load all the compiled files into the interface. Perhaps gzip makes the most sense in this scenario. This will likely have a performance impact, especially for larger specs, as the entire zip has to be downloaded at once / in one go instead of each file asynchronously per the issue. Analyze can probably continue returning JSON regardless.