search

apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint
https://apalache-mc.org/
Apache License 2.0
440 stars 40 forks source link

[FEATURE] Better constant propagation #197

Closed konnov closed 3 years ago

konnov commented 4 years ago

The current optimizer propagates constants, but fails to do so in some cases. For example:

---------------------------- MODULE Opt1 -------------------------------------  
VARIABLES S

A == "Foo"

Init ==
    S = 0

Next ==
    IF A = "Foo"
    THEN S' = 1
    ELSE S' = 2
==============================================================================

The output after the optimization step (as can be seen in out-opt.tla), is like this:

----- MODULE Opt1 -----                                                         

VARIABLE S

Init$0 == S' := 0

Next$0 == "Foo" = "Foo" /\ S' := 1

Next$1 == ~("Foo" = "Foo") /\ S' := 2
===============

It is not clear, why the optimizer did not rewrite "Foo" = "Foo" into TRUE.

The optimizer can be found in at.forsyte.apalache.tla.pp.passes.OptPassImpl.

istoilkovska commented 4 years ago

Equality simplification is defined only for ValEx(TlaInt) and NameEx here.

konnov commented 4 years ago

True. That explains it :D