Swiftpack.co - Package - schaefer-dev/k-bosy

Benchmark files can be found here. Includes both dot graph files and also automata info files.

optionally create xcodeproj from swift package using swift package generate-xcodeproj to work with XCode

Setup

Dependencies

  • EAHyper (AAlta and PLTL supported).
  • Optionally BoSy (Swift) to synthesize strategies from the LTL specifications generated by KBoSy.

Environmet Variables

  • set environment variable EAHYPER_SOLVER_DIR="...../eahyper/LTL_SAT_solver"
  • set environment variable KBOSY_EAHYPER_BINARY="..../eahyper/eahyper_src/eahyper.native"
  • set environment variable KBOSY_OUTPUT_DIR
  • set environment variable KBOSY_ROOT_DIR to absolute path of KBoSy's root directory
  • optionally set environment variable KBOSY_INPUT_DIR to directory to avoid the need to specify absolute paths for both specification, input file and dot-graph
  • adjust BoSy Directory in bosy_run.sh script if it is desired to call BoSy automatically after KBoSy for LTL synthesis

Linux

  • support for Aalta backend in EAHyper, very significant performance benefits due to optimzation for early termination (reports in thesis)
  • Build and run scripts require at least Swift 5.2.4 to be installed

Input

Automata Info Input

  • Specifies which APs are observable and which are not (every AP has to be contained in either of those sets)
  • Specifies KLTL specification that is synthesised by BoSy after knowledge has been abstracted away
  • Specifies Output APs that are under control by the later BoSy-synthesized strategy
  • May specify candidate states for Knowledge terms which would skip the internal model checking to determine this candidate states algorithmically
  • Examples given in Benchmark Repo

Automata Graph Input

  • Needs to mark at least one state as initial state
  • Graph has to be complete, ie. at any point in time every state has to have at least one applicable transition.
  • Transition Conditions have to be given in DNF Form.
  • All APs have to be specified in AutomataInfo File beforehand.
  • Examples given in Benchmark Repo

Most used Arguments

  • -i specifies input automata file. Can be given as relative path starting from the environment variable KBOSY_INPUT_DIR which may be set.
  • -d specifies dot graph of the environmen behavior. Can be given as relative path starting from the environment variable KBOSY_INPUT_DIR which may be set.
  • --benchmark to output performance breakdown of different tasks performed by KBoSy.
  • --synthesize to automatically forward the resulting LTL synthesis task to BoSy.
  • --aalta to use Aalta satifiability checker instead of default PLTL. Results in significant performance improvements as reported in my thesis.

Github

link
Stars: 0

Used By

Total: 0

Releases

Implemented --reduce functionality - 2020-08-22 15:36:30

Ability to simplify LTL assumptions using the --reduce parameter. This will significantly reduce the size of assumptions generated by KBoSy. Useful to synthesize very complex scenarios

Benchmark Support Linux + macOS - 2020-08-13 12:55:53

macOS + Linux Support - 2020-08-13 09:44:51

EAHyper candidate search working - 2020-06-19 10:40:18