apalache-mc/apalache

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

lemmy opened this issue · 8 comments

lemmy commented

Description

Bogus counterexample claiming that {42} \in SUBSET Nat is false.

Input specification

------------------------- MODULE APASubRec ------------------------------           
EXTENDS Integers

VARIABLE
    \* @type: Set(Int);
    v

TypeOK ==
    v \in SUBSET Nat  \*  No bogus counterexample if {42} or Int is substituted for Nat.

Init ==
    v = {42}

Next ==
    UNCHANGED v
==========================================================================

The command line parameters used to run the tool

apalache-mc check --init=Init --next=Next --inv=TypeOK APASubRec.tla

Apalache output 
-> % apalache-0.44.11/bin/apalache-mc check --init=Init --next=Next --inv=TypeOK APASubRec.tla
/Library/Java/JavaVirtualMachines/zulu11.54.25-ca-jdk11.0.14.1-macosx_x64/bin/java -javaagent:/Applications/IntelliJ IDEA CE.app/Contents/lib/idea_rt.jar=53886:/Applications/IntelliJ IDEA CE.app/Contents/bin -Dfile.encoding=UTF-8 -classpath /Users/markus/src/TLA/_community/apalache/mod-tool/target/scala-2.13/classes:/Users/markus/src/TLA/_community/apalache/mod-infra/target/scala-2.13/classes:/Users/markus/src/TLA/_community/apalache/passes/target/scala-2.13/classes:/Users/markus/src/TLA/_community/apalache/shai/target/scala-2.13/classes:/Users/markus/src/TLA/_community/apalache/tla-assignments/target/scala-2.13/classes:/Users/markus/src/TLA/_community/apalache/tla-bmcmt/target/scala-2.13/classes:/Users/markus/src/TLA/_community/apalache/tla-io/target/scala-2.13/classes:/Users/markus/src/TLA/_community/apalache/tla-pp/target/scala-2.13/classes:/Users/markus/src/TLA/_community/apalache/tla-typechecker/target/scala-2.13/classes:/Users/markus/src/TLA/_community/apalache/tlair/target/scala-2.13/classes:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/aopalliance/aopalliance/1.0/aopalliance-1.0.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/ch/qos/logback/logback-classic/1.5.7/logback-classic-1.5.7.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/ch/qos/logback/logback-core/1.5.7/logback-core-1.5.7.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/chuusai/shapeless_2.13/2.3.12/shapeless_2.13-2.3.12.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/github/pureconfig/pureconfig-core_2.13/0.17.7/pureconfig-core_2.13-0.17.7.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/github/pureconfig/pureconfig-generic-base_2.13/0.17.7/pureconfig-generic-base_2.13-0.17.7.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/github/pureconfig/pureconfig-generic_2.13/0.17.7/pureconfig-generic_2.13-0.17.7.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/github/pureconfig/pureconfig_2.13/0.17.7/pureconfig_2.13-0.17.7.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/google/android/annotations/4.1.1.4/annotations-4.1.1.4.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/google/api/grpc/proto-google-common-protos/2.29.0/proto-google-common-protos-2.29.0.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/google/code/findbugs/jsr305/3.0.2/jsr305-3.0.2.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/google/code/gson/gson/2.11.0/gson-2.11.0.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/google/errorprone/error_prone_annotations/2.28.0/error_prone_annotations-2.28.0.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/google/guava/failureaccess/1.0.2/failureaccess-1.0.2.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/google/guava/guava/33.2.1-android/guava-33.2.1-android.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/google/guava/listenablefuture/9999.0-empty-to-avoid-conflict-with-guava/listenablefuture-9999.0-empty-to-avoid-conflict-with-guava.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/google/inject/guice/7.0.0/guice-7.0.0.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/google/j2objc/j2objc-annotations/3.0.0/j2objc-annotations-3.0.0.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/google/protobuf/protobuf-java-util/3.17.2/protobuf-java-util-3.17.2.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/google/protobuf/protobuf-java/3.25.1/protobuf-java-3.25.1.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/lihaoyi/geny_2.13/1.0.0/geny_2.13-1.0.0.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/lihaoyi/ujson_2.13/3.2.0/ujson_2.13-3.2.0.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/lihaoyi/upack_2.13/3.2.0/upack_2.13-3.2.0.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/lihaoyi/upickle-core_2.13/3.2.0/upickle-core_2.13-3.2.0.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/lihaoyi/upickle-implicits_2.13/3.2.0/upickle-implicits_2.13-3.2.0.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/lihaoyi/upickle_2.13/3.2.0/upickle_2.13-3.2.0.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/sun/mail/mailapi/1.6.3/mailapi-1.6.3.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/thesamet/scalapb/zio-grpc/zio-grpc-core_2.13/0.5.3/zio-grpc-core_2.13-0.5.3.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/thesamet/scalapb/lenses_2.13/0.11.17/lenses_2.13-0.11.17.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/thesamet/scalapb/scalapb-runtime-grpc_2.13/0.11.17/scalapb-runtime-grpc_2.13-0.11.17.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/thesamet/scalapb/scalapb-runtime_2.13/0.11.17/scalapb-runtime_2.13-0.11.17.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/typesafe/scala-logging/scala-logging_2.13/3.9.5/scala-logging_2.13-3.9.5.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/com/typesafe/config/1.4.3/config-1.4.3.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/commons-beanutils/commons-beanutils/1.9.4/commons-beanutils-1.9.4.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/commons-collections/commons-collections/3.2.2/commons-collections-3.2.2.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/commons-io/commons-io/2.16.1/commons-io-2.16.1.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/commons-logging/commons-logging/1.3.2/commons-logging-1.3.2.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/dev/zio/izumi-reflect-thirdparty-boopickle-shaded_2.13/2.2.5/izumi-reflect-thirdparty-boopickle-shaded_2.13-2.2.5.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/dev/zio/izumi-reflect_2.13/2.2.5/izumi-reflect_2.13-2.2.5.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/dev/zio/zio-stacktracer_2.13/1.0.18/zio-stacktracer_2.13-1.0.18.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/dev/zio/zio-streams_2.13/1.0.13/zio-streams_2.13-1.0.13.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/dev/zio/zio_2.13/1.0.18/zio_2.13-1.0.18.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/io/grpc/grpc-api/1.66.0/grpc-api-1.66.0.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/io/grpc/grpc-context/1.66.0/grpc-context-1.66.0.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/io/grpc/grpc-core/1.66.0/grpc-core-1.66.0.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/io/grpc/grpc-netty/1.66.0/grpc-netty-1.66.0.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/io/grpc/grpc-protobuf-lite/1.62.2/grpc-protobuf-lite-1.62.2.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/io/grpc/grpc-protobuf/1.62.2/grpc-protobuf-1.62.2.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/io/grpc/grpc-services/1.41.0/grpc-services-1.41.0.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/io/grpc/grpc-stub/1.62.2/grpc-stub-1.62.2.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/io/grpc/grpc-util/1.66.0/grpc-util-1.66.0.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/io/netty/netty-buffer/4.1.100.Final/netty-buffer-4.1.100.Final.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/io/netty/netty-codec-http2/4.1.100.Final/netty-codec-http2-4.1.100.Final.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/io/netty/netty-codec-http/4.1.100.Final/netty-codec-http-4.1.100.Final.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/io/netty/netty-codec-socks/4.1.100.Final/netty-codec-socks-4.1.100.Final.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/io/netty/netty-codec/4.1.100.Final/netty-codec-4.1.100.Final.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/io/netty/netty-common/4.1.100.Final/netty-common-4.1.100.Final.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/io/netty/netty-handler-proxy/4.1.100.Final/netty-handler-proxy-4.1.100.Final.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/io/netty/netty-handler/4.1.100.Final/netty-handler-4.1.100.Final.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/io/netty/netty-resolver/4.1.100.Final/netty-resolver-4.1.100.Final.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/io/netty/netty-transport-native-unix-common/4.1.100.Final/netty-transport-native-unix-common-4.1.100.Final.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/io/netty/netty-transport/4.1.100.Final/netty-transport-4.1.100.Final.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/io/perfmark/perfmark-api/0.27.0/perfmark-api-0.27.0.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/jakarta/inject/jakarta.inject-api/2.0.1/jakarta.inject-api-2.0.1.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/apache/commons/commons-configuration2/2.11.0/commons-configuration2-2.11.0.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/apache/commons/commons-lang3/3.14.0/commons-lang3-3.14.0.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/apache/commons/commons-text/1.12.0/commons-text-1.12.0.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/backuity/clist/clist-core_2.13/3.5.1/clist-core_2.13-3.5.1.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/backuity/clist/clist-macros_2.13/3.5.1/clist-macros_2.13-3.5.1.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/bitbucket/inkytonik/kiama/kiama_2.13/2.5.1/kiama_2.13-2.5.1.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/checkerframework/checker-qual/3.42.0/checker-qual-3.42.0.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/codehaus/mojo/animal-sniffer-annotations/1.24/animal-sniffer-annotations-1.24.jar:/Users/markus/Library/Caches/Coursier/v1/https/oss.sonatype.org/content/repositories/snapshots/org/lamport/tla2tools/1.7.0-SNAPSHOT/tla2tools-1.7.0-20200427.032230-1.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/scala-lang/modules/scala-collection-compat_2.13/2.12.0/scala-collection-compat_2.13-2.12.0.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/scala-lang/modules/scala-collection-contrib_2.13/0.3.0/scala-collection-contrib_2.13-0.3.0.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/scala-lang/modules/scala-parser-combinators_2.13/2.4.0/scala-parser-combinators_2.13-2.4.0.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/scala-lang/scala-library/2.13.14/scala-library-2.13.14.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/scala-lang/scala-reflect/2.13.14/scala-reflect-2.13.14.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/scalaz/scalaz-core_2.13/7.3.5/scalaz-core_2.13-7.3.5.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/slf4j/slf4j-api/2.0.16/slf4j-api-2.0.16.jar:/Users/markus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/tools/aqua/z3-turnkey/4.13.0/z3-turnkey-4.13.0.jar at.forsyte.apalache.tla.Tool --debug check --inv=TypeOK APASubRec.tla
15:01:07.729 [main] INFO at.forsyte.apalache.tla.tooling.opt.CheckCmd -- Loading configuration
15:01:07.802 [main] INFO at.forsyte.apalache.tla.tooling.opt.CheckCmd --   > TLC config file found in specification directory. To enable it, pass --config=APASubRec.cfg.
# Usage statistics is ON. Thank you!
# If you have changed your mind, disable the statistics with config --enable-stats=false.

Output directory: /Users/markus/src/TLA/_community/apalache/_apalache-out/APASubRec.tla/2024-08-21T15-01-08_9395642115140218839
# APALACHE version: v0.45.3-2-g74d01ede9 | build: v0.45.3-2-g74d01ede9 I@15:01:08.526
Tuning: search.outputTraces=false                                 I@15:01:08.639
PASS #0: SanyParser                                               I@15:01:09.399
Not running from fat JAR and APALACHE_HOME is not set;            W@15:01:09.406
will not be able to find the Apalache standard library.           W@15:01:09.407
Parsing file /Users/markus/src/TLA/_community/apalache/APASubRec.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/Integers.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/Naturals.tla
PASS #1: TypeCheckerSnowcat                                       I@15:01:10.132
 > Running Snowcat .::.                                           I@15:01:10.133
 > Your types are purrfect!                                       I@15:01:10.324
 > All expressions are typed                                      I@15:01:10.324
PASS #2: ConfigurationPass                                        I@15:01:10.326
  > Set the initialization predicate to Init                      I@15:01:10.335
  > Set the transition predicate to Next                          I@15:01:10.336
  > Set an invariant to TypeOK                                    I@15:01:10.336
PASS #3: DesugarerPass                                            I@15:01:10.342
  > Desugaring...                                                 I@15:01:10.343
PASS #4: InlinePass                                               I@15:01:10.368
Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Next, TypeOK I@15:01:10.369
PASS #5: TemporalPass                                             I@15:01:10.392
  > Rewriting temporal operators...                               I@15:01:10.392
  > No temporal property specified, nothing to encode             I@15:01:10.392
PASS #6: InlinePass                                               I@15:01:10.393
Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Next, TypeOK I@15:01:10.393
PASS #7: PrimingPass                                              I@15:01:10.399
  > Introducing InitPrimed for Init'                              I@15:01:10.408
PASS #8: VCGen                                                    I@15:01:10.908
  > Producing verification conditions from the invariant TypeOK   I@15:01:10.909
  > VCGen produced 1 verification condition(s)                    I@15:01:10.921
PASS #9: PreprocessingPass                                        I@15:01:10.924
  > Before preprocessing: unique renaming                         I@15:01:10.924
 > Applying standard transformations:                             I@15:01:10.936
  > PrimePropagation                                              I@15:01:10.938
  > Desugarer                                                     I@15:01:10.940
  > UniqueRenamer                                                 I@15:01:10.941
  > Normalizer                                                    I@15:01:10.947
  > Keramelizer                                                   I@15:01:10.951
  > After preprocessing: UniqueRenamer                            I@15:01:10.955
No source location for expr@204: ¬v ∈ SUBSET Nat                  E@15:01:10.965
PASS #10: TransitionFinderPass                                    I@15:01:10.970
  > Found 1 initializing transitions                              I@15:01:10.992
  > Found 1 transitions                                           I@15:01:10.993
  > No constant initializer                                       I@15:01:10.993
  > Applying unique renaming                                      I@15:01:10.994
PASS #11: OptimizationPass                                        I@15:01:10.997
 > Applying optimizations:                                        I@15:01:11.006
  > ConstSimplifier                                               I@15:01:11.007
  > ExprOptimizer                                                 I@15:01:11.009
  > SetMembershipSimplifier                                       I@15:01:11.009
  > ConstSimplifier                                               I@15:01:11.010
PASS #12: AnalysisPass                                            I@15:01:11.012
 > Marking skolemizable existentials and sets to be expanded...   I@15:01:11.016
  > Skolemization                                                 I@15:01:11.017
  > Expansion                                                     I@15:01:11.018
  > Remove unused let-in defs                                     I@15:01:11.019
 > Running analyzers...                                           I@15:01:11.021
  > Introduced expression grades                                  I@15:01:11.024
PASS #13: BoundedChecker                                          I@15:01:11.024
State 0: Checking 1 state invariants                              I@15:01:14.039
Check the trace in: /Users/markus/src/TLA/_community/apalache/_apalache-out/APASubRec.tla/2024-08-21T15-01-08_9395642115140218839/violation1.tla, /Users/markus/src/TLA/_community/apalache/_apalache-out/APASubRec.tla/2024-08-21T15-01-08_9395642115140218839/MCviolation1.out, /Users/markus/src/TLA/_community/apalache/_apalache-out/APASubRec.tla/2024-08-21T15-01-08_9395642115140218839/violation1.json, /Users/markus/src/TLA/_community/apalache/_apalache-out/APASubRec.tla/2024-08-21T15-01-08_9395642115140218839/violation1.itf.json I@15:01:14.386
State 0: state invariant 0 violated.                              I@15:01:14.389
Found 1 error(s)                                                  I@15:01:14.396
The outcome is: Error                                             I@15:01:14.399
Checker has found an error                                        I@15:01:14.407
It took me 0 days  0 hours  0 min  5 sec                          I@15:01:14.407
Total time: 5.859 sec                                             I@15:01:14.407
EXITCODE: ERROR (12)

-> % cat /Users/markus/src/TLA/_specs/MSFT/pbft-tlaplus/_apalache-out/APASubRec.tla/2024-08-17T10-00-12_18056272951489574180/violation1.tla
---------------------------- MODULE counterexample ----------------------------

EXTENDS APASubRec

(* Constant initialization state *)
ConstInit == TRUE

(* Initial state *)
State0 == v = {42}

(* The following formula holds true in the last state and violates the invariant *)
InvariantViolation == ~(v \in SUBSET Nat)

================================================================================
(* Created by Apalache on Sat Aug 17 10:00:14 CEST 2024 *)
(* https://github.com/informalsystems/apalache *)
SMT log 
;; fp.spacer.random_seed = 0
;; nlsat.seed = 0
;; sat.random_seed = 0
;; sls.random_seed = 0
;; smt.random_seed = 0
;; (params seed 0 random_seed 0)
;; declare cell($C$0): CellTFrom(Bool)
(declare-const $C$0 Bool)
(assert (= $C$0 false))
;; declare cell($C$1): CellTFrom(Bool)
(declare-const $C$1 Bool)
(assert (= $C$1 true))
;; declare cell($C$2): CellTFrom(Set(Bool))
(declare-sort Cell_Sb 0)
(declare-const $C$2 Cell_Sb)
;; declare cell($C$3): InfSet[CellTFrom(Int)]
(declare-sort Cell_Zi 0)
(declare-const $C$3 Cell_Zi)
;; declare cell($C$4): InfSet[CellTFrom(Int)]
(declare-const $C$4 Cell_Zi)
;; assert ¬$C$0
(assert (not false))
;; assert $C$1
(assert true)
;; declare edge predicate in_b0_Sb2: Bool
(declare-const in_b0_Sb2 Bool)
;; declare edge predicate in_b1_Sb2: Bool
(declare-const in_b1_Sb2 Bool)
;; assert Apalache!StoreInSet($C$0, $C$2)
(assert in_b0_Sb2)
;; assert Apalache!StoreInSet($C$1, $C$2)
(assert in_b1_Sb2)
(push) ;; becomes 1
(push) ;; becomes 2
; ------- STEP: 0, SMT LEVEL: 2 TRANSITION: 0 {
; AssignmentRule(Apalache!:=(v', {42})) {
; SetCtorRule({42}) {
; IntConstRule(42) {
;; declare cell($C$5): CellTFrom(Int)
(declare-const $C$5 Int)
;; assert $C$5 = 42
(assert (= $C$5 42))
; } IntConstRule returns $C$5 [6 arena cells])
;; declare cell($C$6): CellTFrom(Set(Int))
(declare-sort Cell_Si 0)
(declare-const $C$6 Cell_Si)
;; declare edge predicate in_i5_Si6: Bool
(declare-const in_i5_Si6 Bool)
;; assert Apalache!StoreInSet($C$5, $C$6)
(assert in_i5_Si6)
; } SetCtorRule returns $C$6 [7 arena cells])
; } AssignmentRule returns $C$1 [7 arena cells])
(push) ;; becomes 3
;; assert $C$1
(assert true)
(check-sat)
;; sat = SATISFIABLE
(push) ;; becomes 4
; NegRule(¬v ∈ SUBSET Nat) {
; SetInRule(v ∈ SUBSET Nat) {
; SubstRule(v) {
; } SubstRule returns $C$6 [7 arena cells])
; PowSetCtorRule(SUBSET Nat) {
; BuiltinConstRule(Nat) {
; } BuiltinConstRule returns $C$3 [7 arena cells])
;; declare cell($C$7): PowSet[Set(Int)]
(declare-sort Cell_PSi 0)
(declare-const $C$7 Cell_PSi)
; } PowSetCtorRule returns $C$7 [8 arena cells])
;; declare cell($C$8): CellTFrom(Bool)
(declare-const $C$8 Bool)
;; assert $C$8 = ¬(Apalache!SelectInSet($C$5, $C$6))
(assert (= $C$8 (not in_i5_Si6)))
; } SetInRule returns $C$8 [9 arena cells])
;; declare cell($C$9): CellTFrom(Bool)
(declare-const $C$9 Bool)
;; assert ¬$C$9 = $C$8
(assert (= (not $C$9) $C$8))
; } NegRule returns $C$9 [10 arena cells])
;; assert $C$9
(assert $C$9)
(check-sat)
;; sat = SATISFIABLE
(pop 1) ;; becomes 3
lemmy commented

Disabling the special handling of SUBSET Int in the SetMembershipSimplifier by commenting out the SUBSET case results in Apalache also reporting a bogus counterexample for SUBSET Int. This suggests a bug in handling infinite sets pointing in the direction of PowSetCtorRule.

lemmy commented

More observation:

  • The size of infinite sets like Nat is 0, which results in them being processed by the same branch that handles the empty set:

    apalache/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/LazyEquality.scala

    Lines 303 to 312 in 4f0b30e

    } else if (rightElems.isEmpty) {
    // SE-SUBSETEQ2
    def notIn(le: ArenaCell) = {
    tla.not(tla.selectInSet(le.toBuilder, left.toBuilder))
    }
    val newState = state.updateArena(_.appendCell(BoolT1))
    val pred = newState.arena.topCell
    rewriter.solverContext.assertGroundExpr(tla.eql(pred.toBuilder, tla.and(leftElems.map(notIn): _*)))
    newState.setRex(pred.toBuilder)

  • {} \in SUBSET Nat holds because of

    apalache/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/LazyEquality.scala

    Lines 300 to 302 in 4f0b30e

    if (leftElems.isEmpty) {
    // SE-SUBSETEQ1
    state.setRex(state.arena.cellTrue().toBuilder)

  • {42} \subseteq Nat holds because it is not handled by

    apalache/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/LazyEquality.scala

    Lines 297 to 349 in 4f0b30e

    def subsetEq(state: SymbState, left: ArenaCell, right: ArenaCell): SymbState = {
    val leftElems = state.arena.getHas(left)
    val rightElems = state.arena.getHas(right)
    if (leftElems.isEmpty) {
    // SE-SUBSETEQ1
    state.setRex(state.arena.cellTrue().toBuilder)
    } else if (rightElems.isEmpty) {
    // SE-SUBSETEQ2
    def notIn(le: ArenaCell) = {
    tla.not(tla.selectInSet(le.toBuilder, left.toBuilder))
    }
    val newState = state.updateArena(_.appendCell(BoolT1))
    val pred = newState.arena.topCell
    rewriter.solverContext.assertGroundExpr(tla.eql(pred.toBuilder, tla.and(leftElems.map(notIn): _*)))
    newState.setRex(pred.toBuilder)
    } else {
    // SE-SUBSETEQ3
    var newState = cacheEqConstraints(state, leftElems.cross(rightElems)) // cache all the equalities
    def exists(lelem: ArenaCell) = {
    // inAndEq checks if lelem is in right
    val inAndEqList = rightElems.map(inAndEq(rewriter, _, lelem, right, lazyEq = true))
    // There are plenty of valid subformulas. Simplify!
    simplifier.applySimplifyShallowToBuilderEx(tla.or(inAndEqList: _*))
    }
    def notInOrExists(lelem: ArenaCell) = {
    val notInOrExists =
    simplifier.applySimplifyShallowToBuilderEx(
    tla.or(tla.not(tla.selectInSet(lelem.toBuilder, left.toBuilder)), exists(lelem))
    )
    if (simplifier.isBoolConst(notInOrExists)) {
    notInOrExists // just return the constant
    } else {
    // BUG: this produced OOM on the inductive invariant of Paxos
    // BUGFIX: push this query to the solver, in order to avoid constructing enormous assertions
    newState = newState.updateArena(_.appendCell(BoolT1))
    val pred = newState.arena.topCell
    rewriter.solverContext.assertGroundExpr(simplifier.simplifyShallow(tla.equiv(pred.toBuilder, notInOrExists)))
    pred.toBuilder
    }
    }
    val forEachNotInOrExists =
    simplifier.applySimplifyShallowToBuilderEx(tla.and(leftElems.map(notInOrExists): _*))
    newState = newState.updateArena(_.appendCell(BoolT1))
    val pred = newState.arena.topCell
    rewriter.solverContext.assertGroundExpr(tla.eql(pred.toBuilder, forEachNotInOrExists))
    newState.setRex(pred.toBuilder)
    }
    }
    but is rewritten in \A a \in {42}: a \in Nat by

    apalache/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/Keramelizer.scala

    Lines 99 to 106 in 4f0b30e

    // rewrite A \subseteq B
    // into \A a \in A: a \in B
    case OperEx(TlaSetOper.subseteq, setX, setY) =>
    val elemType = getElemType(setX)
    val tempName = gen.newName()
    tla
    .forall(tla.name(tempName).as(elemType), setX, tla.in(tla.name(tempName).as(elemType), setY).as(BoolT1))
    .as(BoolT1)

    • Rewriting A \subseteq B as A \in SUBSET B (see diff below) triggers the same bug.
diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/Keramelizer.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/Keramelizer.scala
index 6798860e5..91b1163d5 100644
--- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/Keramelizer.scala
+++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/Keramelizer.scala
@@ -99,11 +99,13 @@ class Keramelizer(gen: UniqueNameGenerator, tracker: TransformationTracker)
     // rewrite A \subseteq B
     // into \A a \in A: a \in B
     case OperEx(TlaSetOper.subseteq, setX, setY) =>
-      val elemType = getElemType(setX)
-      val tempName = gen.newName()
-      tla
-        .forall(tla.name(tempName).as(elemType), setX, tla.in(tla.name(tempName).as(elemType), setY).as(BoolT1))
-        .as(BoolT1)
+      val elemType = getElemType(setY)
+      tla.in(setX, tla.powSet(setY).as(elemType)).as(BoolT1)

     // rewrite f \in [S -> SUBSET T]
     // into DOMAIN f = S /\ \A x \in S: \A y \in f[x]: y \in T
lemmy commented

PowSetT has only limited support of finite sets according to its documentation:

apalache/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/types/package.scala

Lines 139 to 153 in d2b5cc2

/**
* The type of a powerset of a finite set, which is constructed as 'SUBSET S' in TLA+.
*
* @param domType
* the type of the argument is a finite set, i.e., typeof(S) in SUBSET S. Currently, only FinSetT(_) is supported.
*/
sealed case class PowSetT(domType: TlaType1) extends CellT with Serializable {
require(domType.isInstanceOf[SetT1]) // currently, we support only PowSetT(FinSetT(_))
override val signature: String = s"P" + CellTFrom(domType).signature
override val toString: String = s"PowSet[$domType]"
override def toTlaType1: TlaType1 = SetT1(domType)
}

thpani commented

For context: the root cause is

apalache/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/PowSetCtorRule.scala

Lines 22 to 29 in d2b5cc2

override def apply(state: SymbState): SymbState = {
state.ex match {
case OperEx(TlaSetOper.powerset, setEx) =>
// switch to cell theory
var nextState = rewriter.rewriteUntilDone(state.setRex(setEx))
val dom = nextState.arena.findCellByNameEx(nextState.ex)
nextState = nextState.updateArena(_.appendCellOld(PowSetT(dom.cellType.toTlaType1)))

This rewrites SUBSET Nat, appending a PowSetT(Set(Int)) cell.

This ends up taking this branch:

apalache/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRule.scala

Lines 58 to 59 in d2b5cc2

case PowSetT(SetT1(_)) =>
powSetIn(setState, setCell, elemCell)

and proceeds as described above in #2948 (comment)

thpani commented

Rewriting A \subseteq B as A \in SUBSET B (see diff below) triggers the same bug.

I'd suggest the opposite: add a case in Keramelizer, analogous to A \subseteq B.

I wonder though why we end up in PowSetCtorRule with Nat in the first place.
@Kukovec @konnov shouldn't we check for that somewhere?

lemmy commented

Rewriting A \subseteq B as A \in SUBSET B (see diff below) triggers the same bug.

I'd suggest the opposite: add a case in Keramelizer, analogous to A \subseteq B.

@thpani I believe this is in the following commit: 027d4c2. However, it doesn't handle more complex scenarios such as (see #2948 (comment)):

------------------------- MODULE APASubRec ------------------------------
EXTENDS Integers

VARIABLE
    \* @type: { p: Set(Int) };
    v

TypeOK ==
    v \in [ p: SUBSET Nat ]  \*  No bogus counterexample if Int is substituted for Nat.

Init ==
    v = [p |-> {42}]

Next ==
    UNCHANGED v
====

I wonder though why we end up in PowSetCtorRule with Nat in the first place.
@Kukovec @konnov shouldn't we check for that somewhere?

The comment in PowSetT stating it only handles finite sets indicates that there might be a more fundamental issue?! That said, LazyEquality#subsetEq could perhaps just branch on right.cellType == InfSetT(CellTFrom(IntT1))?

  • 👍1
lemmy commented

[...] However, it doesn't handle more complex scenarios such as:

------------------------- MODULE APASubRec ------------------------------
EXTENDS Integers

VARIABLE
    \* @type: { p: Set(Int) };
    v

TypeOK ==
    v \in [ p: SUBSET Nat ]  \* Nat \ {0} is also correctly handled.

Init ==
    v = [p |-> {42}]

Next ==
    UNCHANGED v
====

830caa7 makes Apalache correctly handle this spec.

lemmy commented

I wonder though why we end up in PowSetCtorRule with Nat in the first place.
@Kukovec @konnov shouldn't we check for that somewhere?

The comment in PowSetT stating it only handles finite sets indicates that there might be a more fundamental issue?! That said, LazyEquality#subsetEq could perhaps just branch on right.cellType == InfSetT(CellTFrom(IntT1))?

SetInclusionRuleWithFunArraysexplicitly invokes LazyEquality with an infinite set:

apalache/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInclusionRuleWithFunArrays.scala

Lines 34 to 35 in 00d502a

case (CellTFrom(SetT1(_)), InfSetT(_)) =>
rewriter.lazyEq.subsetEq(rightState, leftCell, rightCell)

It appears that the case statement is not covered by any tests, as removing it doesn't lead to any test failures.