informalsystems / apalache Goto Github PK

Currently there is no support for local operators - the solver throws an importer exception.

This class is not used

The class at.forsyte.apalache.tla.assignments.Transformer contains several general-purpose code transformations that should be:

1. Decoupled from the assignments module.
2. Moved to the module tlair, e.g., to the package *.lir.transformers.standard.
3. Made independent from each other. That is, every transformation should be in a separate class and it should be well-documented. Every transformation also should take Map[String, TlaDecl] and return Map[String, TlaDecl]. Hence, we need a trait similar to Transformation, but defined for Map[String, TlaDecl].

The code is obfuscated and not documented

The assignment solver does not look for assignments inside CASE expressions.

CASE  x = 0 -> x' = 1
   [] x = 1 -> x' = 2
   [] OTHER -> x' = 0 

Although we have not found case studies, where CASE is used like that, it should not be hard to add support for such assignments.

For example, expressions of the form C = 1 should automatically be transformed into C \in {1}, but they aren't.

Multiple ASSUME statements trigger IllegalStateException("The context has duplicate keys!") in at.forsyte.apalache.tla.imp.Context.scala

Remove the unused classes. Document the rest.

Refactor EqualityAsContainment, Inline, LetInExplicit, Prime, Transformer, UnchangedExplicit, so they look like PrimePropagation

It looks like the package is not used anymore. Delete.

Introduce an optimization for the expressions: Cardinality(S) >= C and Cardinality <= C, where C is a constant.

On code such as
[msgs EXCEPT ![self] = @ \ {q}]
the importer throws
at.forsyte.apalache.tla.imp.SanyImporterException: Unexpected subclass of tla2sany.ExprOrOpArgNode: class tla2sany.semantic.AtNode

https://oss.sonatype.org/content/repositories/snapshots/org/lamport/tla2tools/1.6.0-SNAPSHOT/

Let me know if you want 1.5.x too

This module will be given arbitrary code and it should not fail on it.

There is a widely-used idiom in TLC that allows one to write tests like follows:

     \/ /\ Print("Starting Test 2", TRUE)
        /\ IF x' = 2 
             THEN y' = 1 
             ELSE Assert(FALSE, "Failed Test 2")

The assignment solver fails to find an assignment for the ELSE branch. One should treat Assert(FALSE, ...) as FALSE. The other kinds of assertions should not be affected.

Handling LET-IN is tedious. Shall we introduce top-level operators instead?

For instance:

A(x) ==
  \E y \in S:
    LET z = x + y IN
      x * y * z

should become:

A_z(x, y) == x + y

A(x) ==
  \E y \in S:
    x * y * A_z(x, y)

Currently, one has to construct TLAEx objects using a variety of operators found in different classes, e.g., OperEx(TlaBoolOper.not, ...) and OperEx(TlaOper.eq, ...).

Let's add an object TlaExBuilder that contains handy constructors for all possible combinations of expressions in LIR.

Collecting expressions and their ids in a singleton is evil, as it stays in memory forever. If you have to map UID to TlaEx, use Map[UID, TlaEx] locally, so the garbage collector could eventually free it.

We have to associate with every expression a pointer to the source code. I believe that can be done using IDs and databases that we designed some time ago.

RecursiveProcessor seems to be a home-brewed lambda calculus inside Scala. Although it is rarely used, its applications are hard to understand. In those rare cases, when RecursiveProcessor is used, instantiate the code directly with the given parameters. It will be much easier to read. For instance, RecursiveProcessor.compute takes 6 parameters, each of them is a parameterized function.

The whole package seems to be to large extent deprecated

Currently, TrivialTypeFinder is keeping type annotations that are given by the user. If an annotated expression is getting rewritten by another expression, TrivialTypeFinder does not propagate the type annotation for the new expression.

We have to introduce a TranformationListener that would listen to code transformations and propagate types.

needs proper constructor and equality check methods, consider migrating to TlaControlOper inner class.

Use a standard library, e.g., a scala version of log4j, to log the operations at different levels

A symbolic state carries a theory (IntTheory, BoolTheory, CellTheory). These theories became irrelevant in the presence of types and the multi-sorted encoding. Remove them.

As type checker is using SourceStore when reporting errors, we have to fix SpecHandler (or whatever unfolds the definitions) to properly track the source code. In the current version, the messages by the type checker are absolutely useless.

When analysis plugins report errors about the source code, they must be reported consistenly, like in a Java/C/... compiler.

This package has collected too many TODOs over time. We have to fix them.

Currently, the assignment finder is looking for assignments in the expressions that match one of two patterns: x = ... or x \in {...}. it is common to use other set relations in TypeOK, e.g., msgs \subseteq Messages. We have to support such subset relations as well. I guess, the latter expression could be simply translated as msgs \in SUBSET(Messages) during the preprocessing phase.

The following code triggers a stack overflow:

java.lang.StackOverflowError: null
	at scala.collection.immutable.List.drop(List.scala:223)
	at scala.collection.immutable.List.drop(List.scala:86)
	at scala.collection.LinearSeqOptimized.apply(LinearSeqOptimized.scala:62)
	at scala.collection.LinearSeqOptimized.apply$(LinearSeqOptimized.scala:61)
	at scala.collection.immutable.List.apply(List.scala:86)
	at at.forsyte.apalache.tla.lir.OperatorHandler$.subAndID$1(OperatorHandler.scala:324)

--------------- MODULE test4 -------------
EXTENDS Naturals, TLC, Sequences
VARIABLE x, y, z, w

Init == 
  /\ Print("Should find only one distinct state", TRUE)
  /\ x = {1, 2, 3}
  /\ y = {"a", "b", "c"}
  /\ z = [a : {1, 2, 3}, b : {1, 2, 3}, c : {1, 2, 3}]
  /\ w = [{1, 2, 3} -> {1, 2, 3}]

Inv  == 
  /\ TRUE
  /\ x = {1, 2, 3}
  /\ y = {"a", "b", "c"}
  /\ z = [a : {1, 2, 3}, b : {1, 2, 3}, c : {1, 2, 3}]
  /\ w = [{1, 2, 3} -> {1, 2, 3}]

Next ==
  \/ /\ x' = {3, 3, 2, 1}
     /\ UNCHANGED <<y, z, w>>
     /\ Print("Test 1", TRUE)
============================================

In some cases, a comparison to an empty set fails. When such a comparison propagates to the level of Z3, the solver complains about incompatible sorts, e.g., comparing Cell_Si to Cell_Su. For instance, check test/tla/Bakery.tla, replace EmptyIntSet == {1} \ {1} with EmptyIntSet == {}.

This problem should be resolved as soon as we have the proper type inference engine.

Add a new operator FAIL(message) that is equivalent to ASSERT(FALSE, message). Use it to implement ASSERT.

The code is hard to read, owing to abuse of anonymous lambdas. Similar to RecursiveProcessor it has to be rewritten or instantiated with concrete parameters.

For some reason, it calls SymbolicTransitionPass inside. The passes should be chained.

It contains too much magic. Remove the unused methods and extract the used methods in separate classes with clear names and documentation.

The purpose of these classes is not clear

The current implementation of toString is producing unreadable output even on small expressions. It makes it impossible to use the output while debugging (see below). There must be a nice way to define various pretty printers in scala.

( OperEx: \cap,
    ( OperEx: {...},
        ( ValEx: TlaInt(1) , id:UID(-1) ),
        ( ValEx: TlaInt(3) , id:UID(-1) ),
      id: UID(-1)
    ),
    ( OperEx: {...},
        ( ValEx: TlaInt(3) , id:UID(-1) ),
        ( ValEx: TlaInt(4) , id:UID(-1) ),
      id: UID(-1)
    ),
  id: UID(-1)
)

There are lots of TODOs and deprecated methods

The new code that assigns names to the variables does not handle declarations inside LET-IN. For instance, see Paxos.tla.