search

will62794 / tla-web

Interactive, web-based environment for exploring TLA+ specifications.
MIT License
64 stars 7 forks source link

Should notify user if spec fails to load #37

Closed hwayne closed 2 months ago

hwayne commented 2 months ago

Two cases I'm thinking of:

  1. Loading a PlusCal file without translation will cause it to spin forever (since it can't translate the pluscal file)
  2. Loading a github link like https://github.com/hwayne/tla-graphing-demo/blob/master/threads.tla will fail because it's not the raw link: you need https://raw.githubusercontent.com/hwayne/tla-graphing-demo/master/threads.tla
will62794 commented 2 months ago

In general, there are a variety of error reporting features that can be improved upon in the tool, but I pushed a few changes that should help address (2) more clearly (i.e. cases where a spec can't be fetched properly from the given URL).

For (1), I believe the tool will currently just report absence of an initial state predicate (Init) as an error if a PlusCal spec is given without any translation. For example, you can try loading this raw spec. There may be some additional edge cases to consider when handling various PlusCal specs, but I haven't thought about it too carefully yet.