Skip to content

LTL checking

LTL checking #1908

name: Linux build-test-deploy
on:
push:
pull_request:
types: [opened, synchronize, reopened]
workflow_dispatch:
inputs:
message:
description: 'Summarize the contents since the last version'
required: true
default: 'Auto-generated release'
permissions: write-all
concurrency:
group: deploy-${{ github.ref }}-${{ github.event_name }}
cancel-in-progress: true
jobs:
build:
runs-on: ubuntu-24.04
steps:
- name: Checkout repository
uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
- name: Build
uses: ./.github/actions/build-action
- name: Upload JARs
uses: actions/upload-artifact@b4b15b8c7c6ac21ea08fcf65892d2ee8f75cf882 # v3.1.2
with:
name: ThetaJars
path: subprojects/**/*-all.jar
- name: Positive outcome badge
uses: ./.github/actions/badge-creation
with:
label: "${{ runner.os }} build"
status: "Success"
color: "green"
path: "badges/build-${{ runner.os }}"
- name: Negative outcome badge
if: ${{ failure() }}
uses: ./.github/actions/badge-creation
with:
label: "${{ runner.os }} build"
status: "Failure"
color: "red"
path: "badges/build-${{ runner.os }}"
test-benchexec:
strategy:
matrix:
rundef:
- SV-COMP25_unreach-call
- SV-COMP25_no-data-race
- SV-COMP25_valid-memcleanup
- SV-COMP25_valid-memsafety
- SV-COMP25_no-overflow
- SV-COMP25_termination
portfolio: [CEGAR, BOUNDED, HORN]
include:
- tool: Theta_SV-COMP
portfolio: CEGAR
- tool: EmergenTheta_SV-COMP
portfolio: BOUNDED
- tool: Thorn_SV-COMP
portfolio: HORN
runs-on: ubuntu-24.04
needs: create-archives
steps:
- name: Checkout repository
uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
- name: Run benchexec
uses: ./.github/actions/benchexec-test
with:
rundef: ${{ matrix.rundef }}
portfolio: ${{ matrix.portfolio }}
tool: ${{ matrix.tool }}
xml: ${{ contains(github.event.pull_request.labels.*.name, 'svcomp') && 'theta.xml' || 'theta-short.xml' }}
timeout: ${{ contains(github.event.pull_request.labels.*.name, 'svcomp') && 3600 || 900 }}
collect-results:
needs: test-benchexec
runs-on: ubuntu-24.04
steps:
- name: Checkout repository
uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
- name: Generate report
uses: ./.github/actions/benchexec-report
create-spec-transformation:
runs-on: ubuntu-24.04
steps:
- name: Checkout repository
uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
- name: Create spec-transformation
uses: ./.github/actions/build-spec-transformation
create-archives:
runs-on: ubuntu-24.04
needs: [build, create-spec-transformation]
strategy:
matrix:
tool: [Theta, EmergenTheta, Thorn]
include:
- tool: Theta
portfolio: STABLE
- tool: EmergenTheta
portfolio: EMERGENT
- tool: Thorn
portfolio: HORN
steps:
- name: Checkout repository
uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
- name: Create ${{matrix.tool}}
uses: ./.github/actions/build-archive
with:
name: ${{matrix.tool}}
inputflag: "--portfolio ${{matrix.portfolio}}"
javadoc:
needs: build
runs-on: ubuntu-24.04
steps:
- name: Checkout repository
uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
- name: Deploy javadoc to github-pages
uses: ./.github/actions/deploy-javadoc
test-linux:
strategy:
fail-fast: false
matrix:
os: [ubuntu-24.04]
needs: build
runs-on: ${{ matrix.os }}
steps:
- name: Checkout repository
uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
- name: Install LLVM and Clang
uses: ./.github/actions/install-llvm
with:
version: "15"
- name: Run tests
uses: ./.github/actions/test-action
- name: Positive outcome badge
if: ${{ matrix.os == 'ubuntu-24.04' }}
uses: ./.github/actions/badge-creation
with:
label: "${{ runner.os }} test"
status: "Success"
color: "green"
path: "badges/test-${{ runner.os }}"
- name: Negative outcome badge
if: ${{ failure() && matrix.os == 'ubuntu-24.04' }}
uses: ./.github/actions/badge-creation
with:
label: "${{ runner.os }} test"
status: "Failure"
color: "red"
path: "badges/test-${{ runner.os }}"
deploy-release:
needs: [test-linux, create-archives]
if: "${{ github.event.inputs.message != '' && github.ref == 'refs/heads/master' && github.event_name != 'pull_request' }}"
runs-on: ubuntu-24.04
steps:
- name: Set java home to java 17
run: |
echo "JAVA_HOME=$(echo $JAVA_HOME_17_X64)" >> $GITHUB_ENV
- name: Checkout repository
uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
- name: Create release and deploy JARs
uses: ./.github/actions/create-release
with:
message: ${{ inputs.message }}
deploy-maven:
# needs: test-linux
if: "${{ github.event.inputs.message != '' && github.ref == 'refs/heads/master' && github.event_name != 'pull_request' }}"
runs-on: ubuntu-24.04
steps:
- name: Checkout repository
uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
- name: Create and publish maven release
uses: ./.github/actions/deploy-maven
with:
OSSRH_PASSWORD: ${{ secrets.OSSRH_PASSWORD }}
OSSRH_USERNAME: ${{ secrets.OSSRH_USERNAME }}
PGP_KEY: ${{ secrets.PGP_KEY }}
PGP_KEY_ID: ${{ secrets.PGP_KEY_ID }}
PGP_PWD: ${{ secrets.PGP_PWD }}
test-docker:
strategy:
matrix:
dockerprojects: ["theta-cfa-cli", "theta-sts-cli", "theta-xsts-cli", "theta-xta-cli", "theta-xcfa-cli"]
runs-on: ubuntu-24.04
steps:
- name: Set java home to java 17
run: |
echo "JAVA_HOME=$(echo $JAVA_HOME_17_X64)" >> $GITHUB_ENV
- name: Checkout repository
uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
- name: Version
id: version
run: |
echo version=$(./gradlew properties --no-daemon --console=plain -q | grep "^version:" | awk '{printf $2}') >> $GITHUB_OUTPUT
- name: docker-login
uses: ./.github/actions/docker-login
with:
username: ${{secrets.DOCKER_USERNAME}}
token: ${{secrets.DOCKER_TOKEN}}
- name: docker-login-ghcr
uses: ./.github/actions/docker-login
with:
registry: ghcr.io
username: ${{github.repository_owner}}
token: ${{secrets.GITHUB_TOKEN}}
- name: Build and publish docker file
uses: ./.github/actions/docker-deploy
with:
project: ${{ matrix.dockerprojects }}
version: ${{ steps.version.outputs.version }}
user-dockerhub: ftsrg
user-ghcr: ftsrg
push: false
deploy-docker:
needs: [test-linux, test-docker]
if: "${{ github.event.inputs.message != '' && github.ref == 'refs/heads/master' && github.event_name != 'pull_request' }}"
strategy:
matrix:
dockerprojects: ["theta-cfa-cli", "theta-sts-cli", "theta-xsts-cli", "theta-xta-cli", "theta-xcfa-cli"]
runs-on: ubuntu-24.04
steps:
- name: Set java home to java 17
run: |
echo "JAVA_HOME=$(echo $JAVA_HOME_17_X64)" >> $GITHUB_ENV
- name: Checkout repository
uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
- name: Version
id: version
run: |
echo version=$(./gradlew properties --no-daemon --console=plain -q | grep "^version:" | awk '{printf $2}') >> $GITHUB_OUTPUT
- name: docker-login
uses: ./.github/actions/docker-login
with:
username: ${{secrets.DOCKER_USERNAME}}
token: ${{secrets.DOCKER_TOKEN}}
- name: docker-login-ghcr
uses: ./.github/actions/docker-login
with:
registry: ghcr.io
username: ${{github.repository_owner}}
token: ${{secrets.GITHUB_TOKEN}}
- name: Build and publish docker file
uses: ./.github/actions/docker-deploy
with:
project: ${{ matrix.dockerprojects }}
version: ${{ steps.version.outputs.version }}
user-dockerhub: ftsrg
user-ghcr: ftsrg
push: true
- name: Docker Hub Description update
uses: peter-evans/dockerhub-description@dc67fad7001ef9e8e3c124cb7a64e16d0a63d864
with:
username: ${{ secrets.DOCKER_USERNAME }}
password: ${{ secrets.DOCKER_TOKEN }}
repository: ftsrg/${{ matrix.dockerprojects }}
deploy-docs:
runs-on: ubuntu-24.04
steps:
- name: Checkout repository
uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
- name: Deploy docs
uses: ./.github/actions/deploy-docs