informalsystems/modelator-py

Issues

• Apalache path has issues on mac cause of the space in path

  #71 opened 2 years ago by udit-gulati
  1

• replace recordclass with dataclass

  #69 opened 2 years ago by rnbguy
  0

• Bump versions in `pyproject.toml`

  #59 opened 2 years ago by rnbguy
  3

• FileNotFoundError exception when apalache command is failed

  #67 opened 2 years ago by rnbguy
  0

• Minimum supported python version

  #64 opened 2 years ago by rnbguy
  0

• Add timeout option to TLC raw

  #56 opened 2 years ago by ivan-gavran
  0

• executable conflict with `modelator`

  #62 opened 2 years ago by rnbguy
  0

• Feature: long term solution for working with TLA+ code (parser)

  #9 opened 3 years ago by danwt
  11

• ImportError: sys.meta_path is None, Python is likely shutting down

  #58 opened 3 years ago by rnbguy
  1

• TLC output parser fails for counterexamples of length 1

  #55 opened 3 years ago by ivan-gavran
  9

• Bug: test_tlc.py hangs

  #53 opened 3 years ago by ivan-gavran
  7

• Feature: tag outputs with version

  #52 opened 3 years ago by danwt
  1

• Feature: support interrupting long processes

  #51 opened 3 years ago by danwt
  0

• Feature: windows support

  #50 opened 3 years ago by danwt
  0

• Feature: sensible model checker defaults

  #49 opened 3 years ago by danwt
  0

• Feature: better cli docs

  #47 opened 3 years ago by danwt
  0

• Improve cli usage docs and library usage samples

  #45 opened 3 years ago by danwt
  1

• Operations: setup continuous automatic releases, version numbers, changelogs

  #15 opened 3 years ago by danwt
  0

• Operations: explore options for publishing the project

  #24 opened 3 years ago by danwt
  3

• Operations: match commit hook versions to pyproject.toml versions

  #2 opened 3 years ago by danwt
  1

• Operations: make git commit hooks automatic, especially for commiting to main

  #23 opened 3 years ago by danwt
  2

• Operations: add git hooks that will delete empty directories when changing branch

  #25 opened 3 years ago by danwt
  1

• Operations: consider additional code quality tools

  #1 opened 3 years ago by danwt
  1

• Feature: reintroduce Apalache functionalities

  #17 opened 3 years ago by danwt
  1

• Feature: smartly acquire model checker jars for use in tests

  #26 opened 3 years ago by danwt
  4

• Feature: ensure that CLI documentation is clear, accurate and informative

  #27 opened 3 years ago by danwt
  1

• Feature: ensure correct JDK used when running Apalache

  #40 opened 3 years ago by danwt
  1

• Feature: update TLC arguments for TLC 2.18

  #39 opened 3 years ago by danwt
  0

• Feature: allow custom JVM arguments for TLC, Apalache

  #38 opened 3 years ago by danwt
  0

• Feature: ensure that the `tlc pure` command does not read too much from the filesystem into memory

  #22 opened 3 years ago by danwt
  1

• Feature: implement a better prototype trace subset selection function

  #36 opened 3 years ago by danwt
  0

• Feature: easily identify trace from list based on binary condition

  #35 opened 3 years ago by danwt
  2

• Feature: quickly get JSON format for a spec

  #6 opened 3 years ago by danwt
  1

• Feature: facilitate progress updates (could be used for progress bars)

  #33 opened 3 years ago by danwt
  0

• Feature: transform traces in the stdout of TLC into Informal Trace Format

  #21 opened 3 years ago by danwt
  1

• Operations: document existence of the recommended VSCode settings

  #16 opened 3 years ago by danwt
  1

• Feature: generate multiple traces for an invariant violation using TLC

  #10 opened 3 years ago by danwt
  0

• Feature: extract list of TLA+ lasso traces from the stdout of TLC

  #18 opened 3 years ago by danwt
  1

• Feature: extract list of TLA+ non-lasso traces from the stdout of TLC

  #13 opened 3 years ago by danwt
  1

• Feature: TLA to JSON functionality for the states inside TLC traces

  #8 opened 3 years ago by danwt
  1

• Operations: retrieve lost branch that includes tla_python

  #20 opened 3 years ago by danwt
  1

• Finalize the name of this repository and the corresponding Python program.

  #12 opened 3 years ago by danwt
  1

• User flow: write predicate operators in a TLA+ spec for which many traces can be generated

  #14 opened 3 years ago by danwt
  1

• Make this repository public.

  #11 opened 3 years ago by danwt
  1

• Determine if `-cleanup` should be passed as a flag to TLC or not when using `tlc pure`.

  #5 opened 3 years ago by danwt
  1

• Determine if the Json trace functionality included with TLC should be used.

  #7 opened 3 years ago by danwt
  1

• Apalache/TLC wrapper API design

  #3 opened 3 years ago by danwt
  5