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
EAHYPER_SOLVER_DIR="...../eahyper/LTL_SAT_solver"
KBOSY_EAHYPER_BINARY="..../eahyper/eahyper_src/eahyper.native"
KBOSY_OUTPUT_DIR
KBOSY_ROOT_DIR
to absolute path of KBoSy's root directoryKBOSY_INPUT_DIR
to directory to avoid the need to specify absolute paths for both specification, input file and dot-graphbosy_run.sh
script if it is desired to call BoSy automatically after KBoSy for LTL synthesis-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.link |
Stars: 0 |
Last commit: 3 years ago |
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
Swiftpack is being maintained by Petr Pavlik | @ptrpavlik | @swiftpackco | API | Analytics