Skip to content

Commit

Permalink
Turn sequential combinations in run config of SV-COMP24 into parallel…
Browse files Browse the repository at this point in the history
… portfolio

The sequences contain configurations for '::if-recursive' and '::if-concurrent'.
These configurations are still set in sequence after the parallel portfolio of
all other techniques.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/svcomp24-parallel-portfolio-approach@45050 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
  • Loading branch information
lemberge committed Nov 8, 2023
1 parent 6457d43 commit da70c21
Show file tree
Hide file tree
Showing 8 changed files with 93 additions and 17 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,6 @@
analysis.restartAfterUnknown = true

# The analyses used for reachability properties.
restartAlgorithm.configFiles = svcomp24--configselection-singleconfig-bmc.properties, \
restartAlgorithm.configFiles = svcomp24--parallel-bmc.properties, \
svcomp24--recursion.properties::if-recursive, \
svcomp24--concurrency.properties::if-concurrent, \
svcomp24--configselection-restartcomponent-predicateAnalysis-end.properties
svcomp24--concurrency.properties::if-concurrent
Original file line number Diff line number Diff line change
Expand Up @@ -15,8 +15,6 @@
analysis.restartAfterUnknown = true

# The analyses used for reachability properties.
restartAlgorithm.configFiles = svcomp24--configselection-restartcomponent-valueAnalysis.properties, \
svcomp24--configselection-restartcomponent-valueAnalysis-itp-end.properties, \
restartAlgorithm.configFiles = svcomp24--parallel-valueAnalysis.properties, \
svcomp24--recursion.properties::if-recursive, \
svcomp24--concurrency.properties::if-concurrent, \
svcomp24--complexLoops-kInduction.properties
svcomp24--concurrency.properties::if-concurrent
6 changes: 1 addition & 5 deletions config/components/svcomp24--multipleLoopsConfig.properties
Original file line number Diff line number Diff line change
Expand Up @@ -19,10 +19,6 @@
analysis.restartAfterUnknown = true

# The analyses used for reachability properties.
restartAlgorithm.configFiles = svcomp24--multipleLoops-symbolicExecution.properties, \
svcomp24--multipleLoops-valueAnalysis-Cegar.properties, \
svcomp24--multipleLoops-predicateAnalysis.properties, \
svcomp24--multipleLoops-dataFlow.properties, \
svcomp24--multipleLoops-kInduction.properties, \
restartAlgorithm.configFiles = svcomp24--parallel-multipleLoops.properties, \
svcomp24--recursion.properties::if-recursive, \
svcomp24--concurrency.properties::if-concurrent
20 changes: 20 additions & 0 deletions config/components/svcomp24--parallel-bmc.properties
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
# This file is part of CPAchecker,
# a tool for configurable software verification:
# https://cpachecker.sosy-lab.org
#
# SPDX-FileCopyrightText: 2023 Dirk Beyer <https://www.sosy-lab.org>
#
# SPDX-License-Identifier: Apache-2.0

# ----------------------------------------------------------------------
# This configuration file uses a parallel portfolio
# of different analyses.
# ----------------------------------------------------------------------

# Use parallel portfolio of analyses
analysis.useParallelAnalyses=true

# The analyses used for reachability properties.
parallelAlgorithm.configFiles = svcomp24--configselection-singleconfig-bmc.properties, \
svcomp24--configselection-restartcomponent-predicateAnalysis-end.properties

23 changes: 23 additions & 0 deletions config/components/svcomp24--parallel-multipleLoops.properties
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
# This file is part of CPAchecker,
# a tool for configurable software verification:
# https://cpachecker.sosy-lab.org
#
# SPDX-FileCopyrightText: 2023 Dirk Beyer <https://www.sosy-lab.org>
#
# SPDX-License-Identifier: Apache-2.0

# ----------------------------------------------------------------------
# This configuration file uses a parallel portfolio
# of different analyses.
# ----------------------------------------------------------------------

# Use parallel portfolio of analyses
analysis.useParallelAnalyses=true

# The analyses used for reachability properties.
parallelAlgorithm.configFiles = svcomp24--multipleLoops-symbolicExecution.properties, \
svcomp24--multipleLoops-valueAnalysis-Cegar.properties, \
svcomp24--multipleLoops-predicateAnalysis.properties, \
svcomp24--multipleLoops-dataFlow.properties, \
svcomp24--multipleLoops-kInduction.properties

23 changes: 23 additions & 0 deletions config/components/svcomp24--parallel-singleLoop.properties
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
# This file is part of CPAchecker,
# a tool for configurable software verification:
# https://cpachecker.sosy-lab.org
#
# SPDX-FileCopyrightText: 2023 Dirk Beyer <https://www.sosy-lab.org>
#
# SPDX-License-Identifier: Apache-2.0

# ----------------------------------------------------------------------
# This configuration file uses a parallel portfolio
# of different analyses.
# ----------------------------------------------------------------------

# Use parallel portfolio of analyses
analysis.useParallelAnalyses=true

# The analyses used for reachability properties.
parallelAlgorithm.configFiles = svcomp24--singleLoop-symbolicExecution.properties, \
svcomp24--singleLoop-valueAnalysis-Cegar.properties, \
svcomp24--singleLoop-predicateAnalysis.properties, \
svcomp24--singleLoop-dataFlow.properties, \
svcomp24--singleLoop-IMC.properties

21 changes: 21 additions & 0 deletions config/components/svcomp24--parallel-valueAnalysis.properties
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
# This file is part of CPAchecker,
# a tool for configurable software verification:
# https://cpachecker.sosy-lab.org
#
# SPDX-FileCopyrightText: 2023 Dirk Beyer <https://www.sosy-lab.org>
#
# SPDX-License-Identifier: Apache-2.0

# ----------------------------------------------------------------------
# This configuration file uses a parallel portfolio
# of different analyses.
# ----------------------------------------------------------------------

# Use parallel portfolio of analyses
analysis.useParallelAnalyses=true

# The analyses used for reachability properties.
parallelAlgorithm.configFiles = svcomp24--configselection-restartcomponent-valueAnalysis.properties, \
svcomp24--configselection-restartcomponent-valueAnalysis-itp-end.properties, \
svcomp24--complexLoops-kInduction.properties

6 changes: 1 addition & 5 deletions config/components/svcomp24--singleLoopConfig.properties
Original file line number Diff line number Diff line change
Expand Up @@ -19,11 +19,7 @@
analysis.restartAfterUnknown = true

# The analyses used for reachability properties.
restartAlgorithm.configFiles = svcomp24--singleLoop-symbolicExecution.properties, \
svcomp24--singleLoop-valueAnalysis-Cegar.properties, \
svcomp24--singleLoop-predicateAnalysis.properties, \
svcomp24--singleLoop-dataFlow.properties, \
svcomp24--singleLoop-IMC.properties, \
restartAlgorithm.configFiles = svcomp24--parallel-singleLoop.properties, \
svcomp24--recursion.properties::if-recursive, \
svcomp24--concurrency.properties::if-concurrent

0 comments on commit da70c21

Please sign in to comment.