Index


  • Introduction

  • Skipped feature combinations
  • Failed test cases
  • Tests by feature combinations
  • SYMMETRY tests
  • Tests under anomalous conditions

  • Tests by feature combinations: -workers 2
  • SYMMETRY tests: -workers 2

  • Tests by feature combinations: -workers auto
  • SYMMETRY tests: -workers auto

SYMMETRY tests; CLI option: -workers 1

SYMMETRY tests, designed to validate important model checker optimization for symmetry sets. These tests also use back-to-back approach, but the only difference between model-under-test and equivalent model is that the latter does not use symmetry set optimization.

Test Cases

Id Type Check Deadlock Invariant Property View Test Results Test Models
287b3e6f5371d71166948f2dbf94a7bca29d0327 TLC with reduction strategy:
  • Do not use SYMMETRY optimization
True True True True Passed
  • Model Under Test
  • Equivalent Model
06a2a634480b7af08dff78205ae42182a31eaa99 TLC with reduction strategy:
  • Do not use SYMMETRY optimization
True True True False Passed
  • Model Under Test
  • Equivalent Model
dc13cf6da0c918867bc31ca8dd07e98daaab2e12 TLC with reduction strategy:
  • Do not use SYMMETRY optimization
True True False True Passed
  • Model Under Test
  • Equivalent Model
88287ec86c9a6404d177865b1f0d4a5c6ee05a5a TLC with reduction strategy:
  • Do not use SYMMETRY optimization
True True False False Passed
  • Model Under Test
  • Equivalent Model
1990846576293477569f267b7490732b74fe4757 TLC with reduction strategy:
  • Do not use SYMMETRY optimization
True False True True Passed
  • Model Under Test
  • Equivalent Model
6a0635676cd8806fdcafbc8beb391b5bd3803f89 TLC with reduction strategy:
  • Do not use SYMMETRY optimization
True False True False Passed
  • Model Under Test
  • Equivalent Model
16a2c4f41e211e9c767f722ca8c4528db778db26 TLC with reduction strategy:
  • Do not use SYMMETRY optimization
True False False True Passed
  • Model Under Test
  • Equivalent Model
a03ea9cfcb654021354ee71fc8e1d4662ced7146 TLC with reduction strategy:
  • Do not use SYMMETRY optimization
True False False False Passed
  • Model Under Test
  • Equivalent Model
796a024daf10f4fa4d39a20c1f096610fae4d459 TLC with reduction strategy:
  • Do not use SYMMETRY optimization
False True True True Passed
  • Model Under Test
  • Equivalent Model
2d7b9d78b65fb745698a0b315cace69ad905f80f TLC with reduction strategy:
  • Do not use SYMMETRY optimization
False True True False Passed
  • Model Under Test
  • Equivalent Model
83e447616b5c6ffae7c731890247697b344d6111 TLC with reduction strategy:
  • Do not use SYMMETRY optimization
False True False True Passed
  • Model Under Test
  • Equivalent Model
54878ea70d5692a29971c91d91d5b24042152208 TLC with reduction strategy:
  • Do not use SYMMETRY optimization
False True False False Passed
  • Model Under Test
  • Equivalent Model
d5b68e9ca220fe298d407c600fea4d7f593459ba TLC with reduction strategy:
  • Do not use SYMMETRY optimization
False False True True Passed
  • Model Under Test
  • Equivalent Model
604fd0db71d619bd9487df0cdd59156e10e1eca8 TLC with reduction strategy:
  • Do not use SYMMETRY optimization
False False True False Passed
  • Model Under Test
  • Equivalent Model
67ccbde8ac65b006fcb33209060a83bfa50b7513 TLC with reduction strategy:
  • Do not use SYMMETRY optimization
False False False True Passed
  • Model Under Test
  • Equivalent Model
2f2f8fe8c975844a1e28f4536b7062e3480fc4e6 TLC with reduction strategy:
  • Do not use SYMMETRY optimization
False False False False Passed
  • Model Under Test
  • Equivalent Model