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 2

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
05484d08b622259a848ae7b9df55a8adfd9c5066 TLC with reduction strategy:
  • Replace `-workers 2` option with the `-workers 1`
True True True True Passed
  • Model Under Test
  • Equivalent Model
e919a448697a04dae81711469486cb8208b815fa TLC with reduction strategy:
  • Replace `-workers 2` option with the `-workers 1`
True True True False Passed
  • Model Under Test
  • Equivalent Model
363c80ac214d45b511ce79ba2c26eb90a4c48705 TLC with reduction strategy:
  • Replace `-workers 2` option with the `-workers 1`
True True False True Passed
  • Model Under Test
  • Equivalent Model
b752f2c8f5ddc5d4d386307b8f00a2926ed6da6e TLC with reduction strategy:
  • Replace `-workers 2` option with the `-workers 1`
True True False False Passed
  • Model Under Test
  • Equivalent Model
f4b2f77abae251bf6d67ecd1ef4450679ef359b6 TLC with reduction strategy:
  • Replace `-workers 2` option with the `-workers 1`
True False True True Passed
  • Model Under Test
  • Equivalent Model
2fb18bfe489be169e0cbd010bb8111f673e231ba TLC with reduction strategy:
  • Replace `-workers 2` option with the `-workers 1`
True False True False Passed
  • Model Under Test
  • Equivalent Model
23c7f6fb5e3996b57a48987183eaebdc95969b24 TLC with reduction strategy:
  • Replace `-workers 2` option with the `-workers 1`
True False False True Passed
  • Model Under Test
  • Equivalent Model
05c8937c77790923b5fc83ba4ba0973cc72a1fe0 TLC with reduction strategy:
  • Replace `-workers 2` option with the `-workers 1`
True False False False Passed
  • Model Under Test
  • Equivalent Model
2cc5659b91288ad5685592ccc0a359e03895094b TLC with reduction strategy:
  • Replace `-workers 2` option with the `-workers 1`
False True True True Passed
  • Model Under Test
  • Equivalent Model
7b34a9e5bf3f1c9da39e0333faa59188a622a4a3 TLC with reduction strategy:
  • Replace `-workers 2` option with the `-workers 1`
False True True False Passed
  • Model Under Test
  • Equivalent Model
bc9f75cecf68453899d31374ad1729badca48873 TLC with reduction strategy:
  • Replace `-workers 2` option with the `-workers 1`
False True False True Passed
  • Model Under Test
  • Equivalent Model
f91b8352341889876e900e92c71c08f3fe52d100 TLC with reduction strategy:
  • Replace `-workers 2` option with the `-workers 1`
False True False False Passed
  • Model Under Test
  • Equivalent Model
b0f74464c95572f37c361f79d89ff237ee1c0073 TLC with reduction strategy:
  • Replace `-workers 2` option with the `-workers 1`
False False True True Passed
  • Model Under Test
  • Equivalent Model
078fd7404f1931e949943e7941c545d8c22cd952 TLC with reduction strategy:
  • Replace `-workers 2` option with the `-workers 1`
False False True False Passed
  • Model Under Test
  • Equivalent Model
0b096b9f0253498e0090532d1471a3f3d9f32b5e TLC with reduction strategy:
  • Replace `-workers 2` option with the `-workers 1`
False False False True Passed
  • Model Under Test
  • Equivalent Model
c6ef64781d28487b3fdf6b5c6956b6fb64bb2321 TLC with reduction strategy:
  • Replace `-workers 2` option with the `-workers 1`
False False False False Passed
  • Model Under Test
  • Equivalent Model