This is the main application component of the ProB based timetable validation tool PlÜS built using the Prob2 Java API. Java 11 or newer is required for using PlÜS.

Current Version: 2.9.0

The application can be configured using environment variables or a properties file. These options can (or have to) be used during development to use local copies of the data and B models.

The properties are defined in two files main.properties and local.properties. main.properties is always loaded before local.properties.

local.properties can be used to set and override configuration options for development. See src/main/resources/local.properties.example for a sample configuration file.

modelpath defines the path to the B models, the default is src/main/resourcesmodels.

dbpath defines the path to the database used to generate the data machines.

solver defines which solver to use, options are prob or mock. Setting solver to prob starts the default ProB 2.0 based solver and mock creates a dummy solver, only useful for development and testing purposes.

NOTE: local.properties should never be under version control.

The path to the models and to the database can also be configured using environment variables:

MODELPATH defines the path to the B models.

DBPATH defines the path to the database used to generate the data machines.

Make sure to initialize the git submodules used in this project.

To run the application you will need a copy of the data and models repositories.

Make sure you are in the correct branch of each repository.

• Run make dist in each repository to generate the files needed for the server.
• Set dbpath/DBPATH to the path of the dist directory in the checkout of the data repository.

DBPATH=../data/philfak-data.sqlite3

• Set modelpath/MODELPATH to the path of the dist directory in the checkout of the models repository.

MODELPATH=../models

The application can be started either by running ./gradlew run or using your IDE.

This project is distributed under the terms of the ISC License.