search

apalache-mc / apalache

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

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

Open lemmy opened 4 weeks ago

lemmy commented 4 weeks ago

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 ```smt ;; 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 3 weeks ago

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 3 weeks ago

More observation:

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 3 weeks ago

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

https://github.com/apalache-mc/apalache/blob/d2b5cc26f1ff0e6211b61b92bb2db5dd9625feca/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/types/package.scala#L139-L153

thpani commented 3 weeks ago

For context: the root cause is

https://github.com/apalache-mc/apalache/blob/d2b5cc26f1ff0e6211b61b92bb2db5dd9625feca/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/PowSetCtorRule.scala#L22-L29

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

This ends up taking this branch:

https://github.com/apalache-mc/apalache/blob/d2b5cc26f1ff0e6211b61b92bb2db5dd9625feca/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRule.scala#L58-L59

and proceeds as described above in https://github.com/apalache-mc/apalache/issues/2948#issuecomment-2303259295

thpani commented 3 weeks ago

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 3 weeks ago

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: https://github.com/apalache-mc/apalache/commit/027d4c2a5fff87635af28b0640c2664fe5d6887d. ~However, it doesn't handle more complex scenarios such as~ (see https://github.com/apalache-mc/apalache/issues/2948#issuecomment-2325102837):

------------------------- 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))?

lemmy commented 1 week ago

[...] 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
====

https://github.com/apalache-mc/apalache/commit/830caa71596caf488b7717b39ba2a4e535ddb779 makes Apalache correctly handle this spec.

lemmy commented 1 week ago

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:

https://github.com/apalache-mc/apalache/blob/00d502aa4c9570e63e16a5666fdca91a838a9d4f/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInclusionRuleWithFunArrays.scala#L34-L35

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