search

apalache-mc / apalache

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

[BUG] Log message is not ideal on exhausting state space that is the image of View #1040

Open danwt opened 3 years ago

danwt commented 3 years ago

Description

When you generate multiple counterexamples with --max-error=k, and a View operator, if it is not possible to generate at least k counterexamples then the log contains this line 'Found a deadlock. No SMT model. E@14:57:23.621', which makes sense but is a bit confusing.

Input specification

------------------------------------ MODULE 2PossibleTraces -----------------------------
(*
There should be only two possible paths for x to reach 3
0 -> 1 -> 3
0 -> 2 -> 3
*)

EXTENDS Integers, FiniteSets, Sequences, TLC

VARIABLES 
    \* @type: Int; 
    x

\* @type: () => Bool;
Init == x = 0

ZeroToOne == x = 0 /\ x' = 1
ZeroToTwo == x = 0 /\ x' = 2
OneToThree == x = 1 /\ x' = 3
TwoToThree == x = 2 /\ x' = 3

ThreePlus == 2 < x /\ x' = x + 1

Next == 
    \/ ZeroToOne
    \/ ZeroToTwo
    \/ OneToThree
    \/ TwoToThree
    \/ ThreePlus

IsThree == 
    LET Desired == x = 3
    IN ~Desired

View == x
===============================================================================

The command line parameters used to run the tool

apalache-mc check --max-error=3 --view=View --inv=IsThree 2PossibleTraces.tla

Expected behavior

A nice log message like 'max counterexamples have been generated for the given view'

Log files

# Tool home: /usr/local
# Package:   /usr/local/mod-distribution/target//apalache-pkg-0.15.12-full.jar
# JVM args:  -Xmx4096m -DTLA-Library=/usr/local/src/tla
#
# APALACHE version 0.15.12 build 05d50b2
#
# WARNING: This tool is in the experimental stage.
#          Please report bugs at: [https://github.com/informalsystems/apalache/issues]
# 
# Usage statistics is ON. Thank you!
# If you have changed your mind, disable the statistics with config --enable-stats=false.

Checker options: filename=2PossibleTraces.tla, init=, next=, inv=IsThree I@15:03:26.784
Tuning:                                                           I@15:03:27.459
PASS #0: SanyParser                                               I@15:03:27.460
Parsing file /Users/danwt/Documents/sandbox-tla/2PossibleTraces.tla
Parsing file /private/var/folders/c5/f5xhs6_d2s3_3xr84_rnyswc0000gn/T/Integers.tla
Parsing file /private/var/folders/c5/f5xhs6_d2s3_3xr84_rnyswc0000gn/T/FiniteSets.tla
Parsing file /private/var/folders/c5/f5xhs6_d2s3_3xr84_rnyswc0000gn/T/Sequences.tla
Parsing file /private/var/folders/c5/f5xhs6_d2s3_3xr84_rnyswc0000gn/T/TLC.tla
Parsing file /private/var/folders/c5/f5xhs6_d2s3_3xr84_rnyswc0000gn/T/Naturals.tla
PASS #1: TypeCheckerSnowcat                                       I@15:03:28.372
 > Running Snowcat .::.                                           I@15:03:28.373
 > Your types are great!                                          I@15:03:28.658
 > All expressions are typed                                      I@15:03:28.659
PASS #2: ConfigurationPass                                        I@15:03:28.739
  > 2PossibleTraces.cfg: Loading TLC configuration                I@15:03:28.745
  > Using the init predicate Init from the TLC config             I@15:03:28.794
  > Using the next predicate Next from the TLC config             I@15:03:28.795
  > Set the initialization predicate to Init                      I@15:03:28.796
  > Set the transition predicate to Next                          I@15:03:28.797
  > Set an invariant to IsThree                                   I@15:03:28.797
PASS #3: DesugarerPass                                            I@15:03:28.870
  > Desugaring...                                                 I@15:03:28.870
PASS #4: UnrollPass                                               I@15:03:28.937
  > Unroller                                                      I@15:03:28.971
PASS #5: InlinePass                                               I@15:03:29.035
  > InlinerOfUserOper                                             I@15:03:29.038
  > Wrap                                                          I@15:03:29.046
  > CallByNameOperatorEmbedder                                    I@15:03:29.049
  > LetInExpander                                                 I@15:03:29.056
  > Unwrap                                                        I@15:03:29.061
  > InlinerOfUserOper                                             I@15:03:29.067
Leaving only relevant operators: CInitPrimed, Init, InitPrimed, IsThree, Next, View I@15:03:29.075
PASS #6: PrimingPass                                              I@15:03:29.121
  > Introducing InitPrimed for Init'                              I@15:03:29.123
PASS #7: VCGen                                                    I@15:03:29.156
  > Producing verification conditions from the invariant IsThree  I@15:03:29.156
  > Using state view View                                         I@15:03:29.156
  > VCGen produced 1 verification condition(s)                    I@15:03:29.162
PASS #8: PreprocessingPass                                        I@15:03:29.204
  > Before preprocessing: unique renaming                         I@15:03:29.204
 > Applying standard transformations:                             I@15:03:29.214
  > PrimePropagation                                              I@15:03:29.215
  > Desugarer                                                     I@15:03:29.253
  > UniqueRenamer                                                 I@15:03:29.326
  > Normalizer                                                    I@15:03:29.368
  > Keramelizer                                                   I@15:03:29.412
  > After preprocessing: UniqueRenamer                            I@15:03:29.455
PASS #9: TransitionFinderPass                                     I@15:03:29.494
  > Found 1 initializing transitions                              I@15:03:29.508
  > Found 5 transitions                                           I@15:03:29.528
  > No constant initializer                                       I@15:03:29.528
  > Applying unique renaming                                      I@15:03:29.529
PASS #10: OptimizationPass                                        I@15:03:29.566
 > Applying optimizations:                                        I@15:03:29.568
  > ConstSimplifier                                               I@15:03:29.569
  > ExprOptimizer                                                 I@15:03:29.571
  > ConstSimplifier                                               I@15:03:29.574
PASS #11: AnalysisPass                                            I@15:03:29.602
 > Marking skolemizable existentials and sets to be expanded...   I@15:03:29.603
  > SkolemizationMarker                                           I@15:03:29.604
  > ExpansionMarker                                               I@15:03:29.605
 > Running analyzers...                                           I@15:03:29.607
  > Introduced expression grades                                  I@15:03:29.638
  > Introduced 5 formula hints                                    I@15:03:29.639
PASS #12: PostTypeCheckerSnowcat                                  I@15:03:29.640
 > Running Snowcat .::.                                           I@15:03:29.640
 > Your types are great!                                          I@15:03:29.718
 > All expressions are typed                                      I@15:03:29.718
PASS #13: BoundedChecker                                          I@15:03:29.753
State 0: Checking 1 state invariants                              I@15:03:31.775
Step 0: picking a transition out of 1 transition(s)               I@15:03:31.780
State 1: Checking 1 state invariants                              I@15:03:31.817
State 1: Checking 1 state invariants                              I@15:03:31.832
Step 1: Transition #2 is disabled                                 I@15:03:31.846
Step 1: Transition #3 is disabled                                 I@15:03:31.858
Step 1: Transition #4 is disabled                                 I@15:03:31.877
Step 1: picking a transition out of 2 transition(s)               I@15:03:31.878
Step 2: Transition #0 is disabled                                 I@15:03:31.905
Step 2: Transition #1 is disabled                                 I@15:03:31.921
State 2: Checking 1 state invariants                              I@15:03:31.936
State 2: state invariant 0 violated. Check the counterexample in: counterexample1.tla, MC1.out, counterexample1.json E@15:03:31.983
State 2: Checking 1 state invariants                              I@15:03:32.021
State 2: state invariant 0 violated. Check the counterexample in: counterexample2.tla, MC2.out, counterexample2.json E@15:03:32.041
Step 2: Transition #4 is disabled                                 I@15:03:32.101
Step 2: picking a transition out of 2 transition(s)               I@15:03:32.101
Step 3: Transition #0 is disabled                                 I@15:03:32.127
Step 3: Transition #1 is disabled                                 I@15:03:32.152
Step 3: Transition #2 is disabled                                 I@15:03:32.171
Step 3: Transition #3 is disabled                                 I@15:03:32.187
Step 3: Transition #4 is disabled                                 I@15:03:32.203
Found a deadlock. No SMT model.                                   E@15:03:32.203
Found 2 error(s)                                                  I@15:03:32.204
The outcome is: Error                                             I@15:03:32.205
Checker has found an error                                        I@15:03:32.206
It took me 0 days  0 hours  0 min  5 sec                          I@15:03:32.207
Total time: 5.556 sec                                             I@15:03:32.208
EXITCODE: ERROR (12)

System information

konnov commented 3 years ago

Ah, that's true. Would you prefer seeing: "No way to extend symbolic computation".

danwt commented 3 years ago

Ah, that's true. Would you prefer seeing: "No way to extend symbolic computation".

I think that's just another phrasing of what is already given. I think the problem is that from the current message it's not very obvious that the deadlock is only occurring because previous solutions have been thrown out. It might make a user think their system model has a deadlock when in fact it doesn't.

thpani commented 2 years ago

With flag --no-deadlock introduced in #1679 this now prints:

All executions are shorter than the provided bound.               W@12:42:41.962
Found 2 error(s)                                                  I@12:42:41.963
The outcome is: ExecutionsTooShort                                I@12:42:41.966

@konnov I'd say this is resolved?

thpani commented 2 years ago

Actually, it's not. With --no-deadlock, Apalache finishes with an OK result, even if there were previous counter-examples:

All executions are shorter than the provided bound.               W@12:50:52.595
Found 2 error(s)                                                  I@12:50:52.598
The outcome is: ExecutionsTooShort                                I@12:50:52.601
Checker reports no error up to computation length 10              I@12:50:52.601
It took me 0 days  0 hours  0 min  4 sec                          I@12:50:52.603
Total time: 4.790 sec                                             I@12:50:52.603
EXITCODE: OK
konnov commented 2 years ago

Oops. The fix was not good then

konnov commented 2 years ago

@shonfeder, given the recent refactoring of the configuration options, what would be the optimal place for doing the following: if --max-error=k is set and k > 1, set --no-deadlock to true.

thpani commented 2 years ago

@shonfeder, given the recent refactoring of the configuration options, what would be the optimal place for doing the following: if --max-error=k is set and k > 1, set --no-deadlock to true.

This is also an issue when passing a transition filter. Maybe deadlock checking should be off by default? All other checks we do (invariants, ...) are off by default.

konnov commented 2 years ago

Given that deadlock detection makes an additional call (and it's is incomplete anyways), it seems to be a good idea to me to set --no-deadlock=true by default.

shonfeder commented 2 years ago

what would be the optimal place for doing the following: if --max-error=k is set and k > 1, set --no-deadlock to true.

Really depends on the program logic. If it is an invariant of anything that takes checker options, then I think it should go in the converstion from configurations to "option groups":

https://github.com/informalsystems/apalache/blob/b39ce05b2f8f51858d6ae5262fe5812a59e7ebaf/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/options.scala#L570-L602