apalache-mc/apalache

Issues

• Labels should not prevent the VC generator from decomposing an invariant

  #3019 opened 2 months ago by konnov
  0

• `VCGenerator` should annotate decomposed invariants

  #2968 opened 3 months ago by konnov
  3

• Pull in updated version of SANY to support Unicode specs

  #2995 opened 2 months ago by ahelwer
  26

• Statistics reporter may cause a core dump

  #3004 opened 2 months ago by konnov
  0

• Do not produce distinct on singleton

  #2964 opened 2 months ago by konnov
  0

• Refactor option configurations

  #2999 opened 2 months ago by konnov
  0

• check: surprising temporal NoError result

  #2985 opened 3 months ago by lucab
  7

• Add statistics output for long-running computations

  #2991 opened 2 months ago by konnov
  0

• Figure out what to do about `random_seed`

  #2989 opened 2 months ago by konnov
  0

• Bogus safety violation checking if a set is a subset of Nat

  #2948 opened 3 months ago by lemmy
  8

• Support for mutually-recursive operators in the type checker

  #2978 opened 3 months ago by konnov
  0

• Apalache seems to cache `Gen` expressions

  #2973 opened 3 months ago by Kukovec
  0

• Unexpected equality test over types CellTFrom(Set(Int)) and InfSet[CellTFrom(Int)]

  #2972 opened 3 months ago by lemmy
  0

• Allow for digits in type aliases

  #2967 opened 3 months ago by konnov
  0

• The "Apalache user manual" link in the README.md file is broken

  #2959 opened 3 months ago by saltiniroberto
  0

• Fix the release pipeline

  #2951 opened 3 months ago by konnov
  2

• Repair `docker-tests`

  #2931 opened 3 months ago by konnov
  0

• Repair `docker-container` workflow

  #2932 opened 3 months ago by konnov
  2

• Repair `Auto Update` workflow

  #2933 opened 3 months ago by konnov
  1

• Clean up safe/unsafe builder usage

  #2934 opened 3 months ago by Kukovec
  0

• Add support for Quint's `allListsUpTo`

  #2906 opened 6 months ago by bugarela
  0

• Assignments in quint `init` operators need to be unprimed

  #2863 opened 8 months ago by shonfeder
  2

• TLA+ pretty printer produces `[]` on empty tuples, which is invalid syntax

  #2875 opened 8 months ago by bugarela
  0

• Pretty printing the apalache IR into TLA+ does not sanitize identifiers

  #2858 opened 8 months ago by shonfeder
  0

• Extend the server to be able to reply with formatted TLA+ generated from the IR

  #2851 opened 9 months ago by shonfeder
  1

• Use `parse` to format modules.

  #2797 opened 9 months ago by lemmy
  2

• Name clash leads to operator being incorrectly marked as recursive

  #2826 opened 10 months ago by fan-tom
  3

• Unhandled Exception (java.util.NoSuchElementException: None.get) on empty file input

  #2800 opened 10 months ago by lemmy
  4

• Allow specifying types in separate files

  #2820 opened 10 months ago by nano-o
  0

• Include constant value assignments in ITF

  #2819 opened 10 months ago by shonfeder
  0

• Typechecking crashes with `IllegalArgumentException: Unsupported expression` on unbounded quantification (e.g., `\A x: P`).

  #2816 opened 10 months ago by nano-o
  8

• Operator overriding in annotations

  #2818 opened 10 months ago by konnov
  0

• Crash with `funArrays` encoding

  #2810 opened 10 months ago by nano-o
  2

• `parse` command adds superfluous `EXTENDS` statement

  #2796 opened a year ago by lemmy
  2

• Nix Package

  #2715 opened a year ago by lorenzleutgeb
  8

• Raise error when an unexpanded type constant is found in quint IR output

  #2788 opened a year ago by shonfeder
  0

• Add warning for misplaced occurrence of `oneOf` when parsing from quint

  #2774 opened a year ago by shonfeder
  0

• Wrong function sets counterexample?

  #2772 opened a year ago by Kukovec
  6

• A set filter over PowSet[FinSet[Int]] is not implemented

  #2762 opened a year ago by thpani
  0

• Unexpected exception

  #2750 opened a year ago by konnov
  2

• Document Apalache config format + options

  #2756 opened a year ago by thpani
  0

• BMC pass throws `TypingException`

  #2747 opened a year ago by thpani
  0

• Temporal translation broken with nested temporal subformulas and quantifiers

  #2746 opened a year ago by thpani
  6

• Revise the ITF format

  #2732 opened a year ago by konnov
  0

• Spec rejected due to being outside ReTLA throws stack trace instead of exiting cleanly

  #2713 opened a year ago by Kukovec
  1

• Rework `Oracle`s to be compatible with the new `StratifiedRule` interfaces

  #2708 opened a year ago by Kukovec
  0

• Stratified rules: Integer literals

  #2705 opened a year ago by Kukovec
  0

• Constraints applied to a set created with `Gen(_)` are ignored

  #2702 opened a year ago by Kukovec
  5

• Introduce an operator for bounded sequences

  #2699 opened a year ago by konnov
  0

• GH pages TLS certificate expired

  #2691 opened a year ago by thpani
  1