[BUG] Property in .cfg silently ignored

[lemmy]

Apalache should, perhaps, raise a big fat warning instead of silently ignoring Properties in .cfg?

----------------------------- MODULE Github484 -----------------------------
VARIABLE x

Init == 
  /\ x \in {1}
  
Next == 
  /\ x' \in {1}

Spec ==
  /\ Init
  /\ [][Next]_x

Prop ==
  [](x # 1)
=============================================================================

SPECIFICATION
Spec
PROPERTIES   
Prop

markus@avocado:~/src/TLA/_specs/models/tlcbugs/Github484/Github484.toolbox/Model_1$ /opt/apalache/bin/apalache-mc --config=MC.cfg check MC
# Tool home: /opt/apalache
# Package:   /opt/apalache/mod-distribution/target/apalache-pkg-0.7.2-RELEASE-full.jar
# JVM args: -Xmx4096m -Djava.library.path=/usr/lib/x86_64-linux-gnu/jni/  -DTLA-Library=
#
# APALACHE version 0.7.2-RELEASE build v0.7.1-5-g5b85083
#
# WARNING: This tool is in the experimental stage.
#          Please report bugs at: [https://github.com/informalsystems/apalache/issues]

Checker options: filename=MC, init=, next=, inv=                  I@20:40:09.896
WARNING: An illegal reflective access operation has occurred
WARNING: Illegal reflective access by com.google.inject.internal.cglib.core.$ReflectUtils$1 (file:/opt/apalache/mod-distribution/target/apalache-pkg-0.7.2-RELEASE-full.jar) to method java.lang.ClassLoader.defineClass(java.lang.String,byte[],int,int,java.security.ProtectionDomain)
WARNING: Please consider reporting this to the maintainers of com.google.inject.internal.cglib.core.$ReflectUtils$1
WARNING: Use --illegal-access=warn to enable warnings of further illegal reflective access operations
WARNING: All illegal access operations will be denied in a future release
PASS #0: SanyParser                                               I@20:40:10.231
Parsing file /home/markus/src/TLA/_specs/models/tlcbugs/Github484/Github484.toolbox/Model_1/MC.tla
Parsing file /home/markus/src/TLA/_specs/models/tlcbugs/Github484/Github484.toolbox/Model_1/Github484.tla
Parsing file /tmp/TLC.tla
Parsing file /tmp/Naturals.tla
Parsing file /tmp/Sequences.tla
Parsing file /tmp/FiniteSets.tla
PASS #1: ConfigurationPass                                        I@20:40:10.510
  > Loading TLC configuration from MC.cfg                         I@20:40:10.511
  > Temporal spec found in MC.cfg, which is not yet supported. Skipping. W@20:40:10.574
PASS #2: UnrollPass                                               I@20:40:10.595
  > Unroller                                                      I@20:40:10.597
PASS #3: InlinePass                                               I@20:40:10.616
  > InlinerOfUserOper                                             I@20:40:10.617
  > LetInExpander                                                 I@20:40:10.622
PASS #4: PrimingPass                                              I@20:40:10.632
  > Introducing InitPrimed for Init'                              I@20:40:10.635
PASS #5: VCGen                                                    I@20:40:10.646
  > No invariant given. Only deadlocks will be checked            I@20:40:10.647
PASS #6: PreprocessingPass                                        I@20:40:10.652
  > Before preprocessing: unique renaming                         I@20:40:10.652
 > Applying standard transformations:                             I@20:40:10.657
  > Desugarer                                                     I@20:40:10.658
  > UniqueRenamer                                                 I@20:40:10.662
  > Normalizer                                                    I@20:40:10.687
  > Keramelizer                                                   I@20:40:10.689
  > After preprocessing: UniqueRenamer                            I@20:40:10.695
PASS #7: TransitionFinderPass                                     I@20:40:10.713
  > Found 1 initializing transitions                              I@20:40:10.785
  > Found 1 transitions                                           I@20:40:10.801
  > No constant initializer                                       I@20:40:10.801
  > Applying unique renaming                                      I@20:40:10.802
PASS #8: OptimizationPass                                         I@20:40:10.808
 > Applying optimizations:                                        I@20:40:10.812
  > ConstSimplifier                                               I@20:40:10.813
  > ExprOptimizer                                                 I@20:40:10.815
  > ConstSimplifier                                               I@20:40:10.817
PASS #9: AnalysisPass                                             I@20:40:10.822
 > Marking skolemizable existentials and sets to be expanded...   I@20:40:10.824
  > SkolemizationMarker                                           I@20:40:10.825
  > ExpansionMarker                                               I@20:40:10.827
 > Running analyzers...                                           I@20:40:10.829
  > Introduced expression grades                                  I@20:40:10.835
  > Introduced 2 formula hints                                    I@20:40:10.836
PASS #10: BoundedChecker                                          I@20:40:10.836
No CONSTANT initializer given                                     I@20:40:10.899
Step 0, level 0: checking if 1 transition(s) are enabled and violate the invariant I@20:40:10.905
Step 0, level 1: collecting 1 enabled transition(s)               I@20:40:10.975
Step 1, level 1: checking if 1 transition(s) are enabled and violate the invariant I@20:40:10.991
Step 1, level 2: collecting 1 enabled transition(s)               I@20:40:11.001
Step 2, level 2: checking if 1 transition(s) are enabled and violate the invariant I@20:40:11.011
Step 2, level 3: collecting 1 enabled transition(s)               I@20:40:11.020
Step 3, level 3: checking if 1 transition(s) are enabled and violate the invariant I@20:40:11.028
Step 3, level 4: collecting 1 enabled transition(s)               I@20:40:11.035
Step 4, level 4: checking if 1 transition(s) are enabled and violate the invariant I@20:40:11.045
Step 4, level 5: collecting 1 enabled transition(s)               I@20:40:11.053
Step 5, level 5: checking if 1 transition(s) are enabled and violate the invariant I@20:40:11.059
Step 5, level 6: collecting 1 enabled transition(s)               I@20:40:11.065
Step 6, level 6: checking if 1 transition(s) are enabled and violate the invariant I@20:40:11.073
Step 6, level 7: collecting 1 enabled transition(s)               I@20:40:11.080
Step 7, level 7: checking if 1 transition(s) are enabled and violate the invariant I@20:40:11.094
Step 7, level 8: collecting 1 enabled transition(s)               I@20:40:11.103
Step 8, level 8: checking if 1 transition(s) are enabled and violate the invariant I@20:40:11.114
Step 8, level 9: collecting 1 enabled transition(s)               I@20:40:11.120
Step 9, level 9: checking if 1 transition(s) are enabled and violate the invariant I@20:40:11.131
Step 9, level 10: collecting 1 enabled transition(s)              I@20:40:11.139
Step 10, level 10: checking if 1 transition(s) are enabled and violate the invariant I@20:40:11.146
Step 10, level 11: collecting 1 enabled transition(s)             I@20:40:11.152
The outcome is: NoError                                           I@20:40:11.165                      
PASS #11: Terminal                                                I@20:40:11.167
Checker reports no error up to computation length 10              I@20:40:11.167
It took me 0 days  0 hours  0 min  1 sec                          I@20:40:11.167
Total time: 1.334 sec                                             I@20:40:11.167
EXITCODE: OK

[konnov]

I have started to do a quick fix. That needs some integration tests.

[konnov]

Apalache is now warning the user that PROPERTY is ignored. Also, SPECIFICATION is supported.