diff --git a/.travis.yml b/.travis.yml index 6f6021c..7c9e982 100755 --- a/.travis.yml +++ b/.travis.yml @@ -1,50 +1,40 @@ -# Documentation: http://docs.travis-ci.com/user/languages/julia/ -language: julia -os: - - linux -julia: - - 1.0 - - 1.1 - - nightly - -env: - - CONDA_JL_VERSION="3" PYTHON="" - -addons: - apt: - sources: - - ubuntu-toolchain-r-test - packages: - - g++-7 - - python3-dev - - clang-3.9 - - graphviz - -matrix: - allow_failures: - - julia: nightly - fast_finish: true - -notifications: - email: false -before_script: - - sudo apt-get -qq update - - sudo apt-get install -y pdf2svg - - sudo apt-get install -y texlive-latex-base - - sudo apt-get install -y texlive-binaries - - sudo apt-get install -y texlive-pictures - - sudo apt-get install -y texlive-latex-extra - - sudo pip install dot2tex - # Every 30 seconds, look for the build log file. If it exists, then - # start watching its contents and printing them to stdout as they - # change. This has two effects: - # 1. it avoids Travis timing out because the build outputs nothing - # 2. it makes it more obvious what part of the build, if any, gets stuck - - while sleep 3; do tail ~/build/sisl/Spot.jl/deps/build.log -f ; done & - - sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-7 90 -script: - - if [[ -a .git/shallow ]]; then git fetch --unshallow; fi - - julia --project --color=yes -e 'import Pkg; Pkg.build(); Pkg.test(coverage=true)' -after_success: - - julia --project -e 'import Pkg; Pkg.add("Coverage"); using Coverage; Coveralls.submit(Coveralls.process_folder())' - - julia --project -e 'import Pkg; Pkg.add("Coverage"); using Coverage; Codecov.submit(Codecov.process_folder())' + +# Documentation: http://docs.travis-ci.com/user/languages/julia/ +language: julia +os: + - linux +julia: + - 1.2 + - nightly + +addons: + apt: + sources: + - ubuntu-toolchain-r-test + packages: + - g++-7 + - clang-3.9 + - graphviz + +matrix: + allow_failures: + - julia: nightly + fast_finish: true + +notifications: + email: false +before_script: + - sudo apt-get -qq update + - sudo apt-get install -y pdf2svg + - sudo apt-get install -y texlive-latex-base + - sudo apt-get install -y texlive-binaries + - sudo apt-get install -y texlive-pictures + - sudo apt-get install -y texlive-latex-extra + - sudo pip install dot2tex + - sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-7 90 +script: + - if [[ -a .git/shallow ]]; then git fetch --unshallow; fi + - julia --project --color=yes -e 'import Pkg; Pkg.build(); Pkg.test(coverage=true)' +after_success: + - julia --project -e 'import Pkg; Pkg.add("Coverage"); using Coverage; Coveralls.submit(Coveralls.process_folder())' + - julia --project -e 'import Pkg; Pkg.add("Coverage"); using Coverage; Codecov.submit(Codecov.process_folder())' \ No newline at end of file diff --git a/Project.toml b/Project.toml index aa64058..d6ff5e5 100755 --- a/Project.toml +++ b/Project.toml @@ -4,11 +4,14 @@ repo = "https://github.com/sisl/Spot.jl" version = "0.0.0" [deps] -Conda = "8f4d0f93-b110-5947-807f-2305c1781a2d" +BinaryProvider = "b99e7846-7c00-51b0-8f62-c81ae34c0232" +Cxx = "a0b5b9ef-44b7-5148-a2d1-f6db19f3c3d2" +LaTeXStrings = "b964fa9f-0449-5b57-a5c2-d3ea65f4040f" +Libdl = "8f399da3-3557-5675-b5ff-fb832c97cbdb" LightGraphs = "093fc24a-ae57-5d10-9952-331d41423f4d" MetaGraphs = "626554b9-1ddb-594c-aa3c-2596fe9399a5" Parameters = "d96e819e-fc66-5662-9728-84c9c7592b0a" -PyCall = "438e738f-606a-5dbb-bf0a-cddfbfd45ab0" +Pkg = "44cfe95a-1eb2-52ea-b672-e2afdf69b78f" TikzPictures = "37f6aa50-8035-52d0-81c2-5a1d08754b2d" [extras] @@ -16,4 +19,4 @@ NBInclude = "0db19996-df87-5ea3-a455-e3a50d440464" Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40" [targets] -test = ["NBInclude", "Test"] \ No newline at end of file +test = ["NBInclude", "Test"] diff --git a/README.md b/README.md index db73b6f..0a704b1 100755 --- a/README.md +++ b/README.md @@ -4,19 +4,19 @@ [![CodeCov](https://codecov.io/gh/sisl/Spot.jl/branch/master/graph/badge.svg)](https://codecov.io/gh/sisl/Spot.jl) [![Coveralls](https://coveralls.io/repos/github/sisl/Spot.jl/badge.svg?branch=master)](https://coveralls.io/github/sisl/Spot.jl?branch=master) -This package provides Julia bindings to the [Spot](https://spot.lrde.epita.fr/index.html) library for LTL and automata manipulation. -It requires the python bindings of spot to be correctly installed and accessible via [PyCall.jl](https://github.com/JuliaPy/PyCall.jl) +This package provides Julia bindings to the [Spot](https://spot.lrde.epita.fr/index.html) library for LTL and automata manipulation. It relies on [Cxx.jl](https://github.com/JuliaInterop/Cxx.jl) to interface julia with the Spot c++ library. + +If you wish to use `PyCall` instead and interact with the spot python bindings you should checkout the branch `pycall` (linux only). ## Installation -For the rendering, Spot requires [GraphViz](https://graphviz.gitlab.io/) and [dot2tex](https://dot2tex.readthedocs.io/en/latest/index.html) to be installed. +For the rendering, Spot requires [GraphViz](https://graphviz.gitlab.io/) and [dot2tex](https://dot2tex.readthedocs.io/en/latest/index.html) to be installed. In addition, the precompile binaries require `gcc` 7 or 8 (not needed for Mac). ```julia using Pkg; Pkg.add("https://github.com/sisl/Spot.jl") ``` -Python dependencies: - - IPython (for visualization in jupyter notebook) +**Windows support:** The registered version of Cxx.jl is currently broken for Windows. However, the branch `gn-patch-crash` is working for now. The build script should checkout the right branch. Otherwise run `] add Cxx#gn-patch-crash` in the julia environment where you wish to install Spot. ## Usage @@ -46,11 +46,11 @@ a = translate(translator, ltl) A basic tutorial is available in [docs/spot_basic_tutorial.ipynb](https://github.com/sisl/Spot.jl/blob/master/docs/spot_basic_tutorial.ipynb) +### Notes -## TODOs - -- [ ] Use CXXWrap.jl to avoid relying on a third language (python) and automatically import all the spot functions. -- [ ] Try using BinaryBuilder. A first experiment was not successful, the path to `libspot.so` in the python bindings is wrong. +Right now, the wrapping of all the c++ functions present in `libspot` is not automatic. +Every function can be called using the Cxx interface. +If you need to wrap a function that has not been wrapped yet, feel free to submit a Pull Request. ## Acknowledgement diff --git a/deps/build.jl b/deps/build.jl index a1abaab..2fe0c0d 100755 --- a/deps/build.jl +++ b/deps/build.jl @@ -1,62 +1,45 @@ -using PyCall -using Conda +using BinaryProvider # requires BinaryProvider 0.3.0 or later -const SPOT_DEV_URL = "https://gitlab.lrde.epita.fr/spot/spot/-/jobs/21743/artifacts/download" -# const SPOT_DEV_URL = "https://gitlab.lrde.epita.fr/spot/spot/-/jobs/21303/artifacts/download" +# Parse some basic command-line arguments +const verbose = "--verbose" in ARGS +const prefix = Prefix(get([a for a in ARGS if a != "--verbose"], 1, joinpath(@__DIR__, "usr"))) +products = [ + LibraryProduct(prefix, ["libspot"], :libspot), +] -const SPOT_VERSION = "spot-2.6.3.dev" -const GCC_MAJOR_VERSION = parse(Int,Char(read(`g++ -dumpversion | cut -f1 -d.`)[1])) # get g++ major version +if Sys.iswindows() + using Pkg + Pkg.add(PackageSpec(name="Cxx", rev="gn-patch-crash")) +end + +# Download binaries from hosted location +bin_prefix = "https://github.com/MaximeBouton/SpotBuilder/releases/download/v2.8.1" -if !Sys.isunix() - throw("Windows not supported") +# Listing of files generated by BinaryBuilder: +download_info = Dict( + MacOS(:x86_64) => ("$bin_prefix/Spot.v2.8.1.x86_64-apple-darwin14.tar.gz", "de9236acab1975a06f218d2939f6c319fb0bc67546e89cdc5c85ef90be509cb4"), + Linux(:x86_64, libc=:glibc, compiler_abi=CompilerABI(:gcc7)) => ("$bin_prefix/Spot.v2.8.1.x86_64-linux-gnu-gcc7.tar.gz", "2fd4429180f94e67284ae37704aa22bed357e2a356062f8af0cd39397a173f4c"), + Linux(:x86_64, libc=:glibc, compiler_abi=CompilerABI(:gcc8)) => ("$bin_prefix/Spot.v2.8.1.x86_64-linux-gnu-gcc8.tar.gz", "7caaa648e059c354892a5503b30bf3b2d368469b4295f54564f8a212fa3e2893"), + Windows(:x86_64, compiler_abi=CompilerABI(:gcc7)) => ("$bin_prefix/Spot.v2.8.1.x86_64-w64-mingw32-gcc7.tar.gz", "782f52898e81c51abd8930c34184a6f99d78e4a49e7a6c753b9eb0741e8bcdfc"), + Windows(:x86_64, compiler_abi=CompilerABI(:gcc8)) => ("$bin_prefix/Spot.v2.8.1.x86_64-w64-mingw32-gcc8.tar.gz", "283473593d120f968366f85da52bd4341ac94715c49476adf9bdd1688b445411"), +) + +# Install unsatisfied or updated dependencies: +unsatisfied = any(!satisfied(p; verbose=verbose) for p in products) +dl_info = choose_download(download_info, platform_key_abi()) +if dl_info === nothing && unsatisfied + # If we don't have a compatible .tar.gz to download, complain. + # Alternatively, you could attempt to install from a separate provider, + # build from source or something even more ambitious here. + error("Your platform (\"$(Sys.MACHINE)\", parsed as \"$(triplet(platform_key_abi()))\") is not supported by this package!") end -# borrowed from TensorFlow.jl -if PyCall.conda - println("Building Spot from source...") - pyversion = PyCall.pyversion - base = dirname(@__FILE__) - println("Switching to directory $base") - cd(base) - isfile("$SPOT_VERSION.zip") ? nothing : run(`wget -O $SPOT_VERSION.zip $SPOT_DEV_URL`) - run(`unzip $SPOT_VERSION.zip`) - run(`rm $SPOT_VERSION.zip`) - run(`tar -xzf $SPOT_VERSION.tar.gz`) # extract - isdir("spot") ? mkdir("spot") : nothing - cd(SPOT_VERSION) - if GCC_MAJOR_VERSION < 5 - println("g++ version must be at least 5.0.0") - end - run(`./configure CXX=g++-7 PYTHON=$(Conda.PYTHONDIR)/python --prefix $(joinpath(base, "spot"))`) - run(`make`) - run(`make install`) - println(readdir(joinpath(base, "spot", "lib"))) - @assert isdir(joinpath(base, "spot")) - @assert isdir(joinpath(base, "spot", "lib", "python"*string(pyversion.major)*"."*string(pyversion.minor), "site-packages")) - println("Python bindings located at: ", joinpath(base, "spot", "lib", "python"*string(pyversion.major)*"."*string(pyversion.minor), "site-packages")) - println("build successful") - println("Linking python bindings to Conda.jl") - conda_path = joinpath(Conda.ROOTENV, "lib", "python"*string(pyversion.major)*"."*string(pyversion.minor), "site-packages") - pythonspot = joinpath(base, "spot", "lib","python"*string(pyversion.major)*"."*string(pyversion.minor), "site-packages") - cd(conda_path) - run(`ln -sf $pythonspot/spot`) - run(`ln -sf $pythonspot/_buddy.a`) - run(`ln -sf $pythonspot/_buddy.la`) - run(`ln -sf $pythonspot/_buddy.so`) - run(`ln -sf $pythonspot/buddy.py`) -else - try - pyimport("spot") - catch ee - typeof(ee) <: PyCall.PyError || rethrow(ee) - error(""" -Python Spot not installed -Please either: - - Rebuild PyCall to use Conda, by running in the julia REPL: - - `ENV["PYTHON"]=""; Pkg.build("PyCall"); Pkg.build("Spot")` - - Or install the python binding yourself: - Install Spot from https://spot.lrde.epita.fr/install.html - Find the python bindings in path/to/spot/lib/python3.x/site-packages -""") - end +# If we have a download, and we are unsatisfied (or the version we're +# trying to install is not itself installed) then load it up! +if unsatisfied || !isinstalled(dl_info...; prefix=prefix) + # Download and install binaries + install(dl_info...; prefix=prefix, force=true, verbose=verbose) end + +# Write out a deps.jl file that will contain mappings for our products +write_deps_file(joinpath(@__DIR__, "deps.jl"), products, verbose=verbose) diff --git a/docs/spot_basic_tutorial.ipynb b/docs/spot_basic_tutorial.ipynb index 4bc08db..2606821 100644 --- a/docs/spot_basic_tutorial.ipynb +++ b/docs/spot_basic_tutorial.ipynb @@ -8,7 +8,7 @@ "\n", "Spot.jl is a wrapper for the [Spot](https://spot.lrde.epita.fr/index.html) library. \n", "\n", - "It is using [PyCall.jl](https://github.com/JuliaPy/PyCall.jl) under the hood and any Spot function from the python bindings can be used in Julia via the PyCall interface. A few functions have been reimplemented to manipulate automatas as pure Julia objects (e.g. `DeterministicRabinAutomata`). \n", + "It is using [Cxx.jl](https://github.com/JuliaInterop/Cxx.jl) under the hood and any Spot function can be used in Julia via the Cxx interface. A few functions have been reimplemented to manipulate automatas as pure Julia objects (e.g. `DeterministicRabinAutomata`). \n", "\n", "For more extensive tutorials see the original [Spot documentation](https://spot.lrde.epita.fr/tut.html).\n" ] @@ -22,7 +22,11 @@ "name": "stderr", "output_type": "stream", "text": [ - "┌ Info: Recompiling stale cache file /mnt/c/Users/Maxime/wsl/.julia/compiled/v1.1/Spot/dk13t.ji for Spot [f11abc24-ce50-11e8-2475-af6658d13f2b]\n", + "┌ Info: Precompiling Spot [f11abc24-ce50-11e8-2475-af6658d13f2b]\n", + "└ @ Base loading.jl:1186\n", + "┌ Info: Recompiling stale cache file C:\\Users\\Maxime\\.julia\\compiled\\v1.1\\Cxx\\ESGkI.ji for Cxx [a0b5b9ef-44b7-5148-a2d1-f6db19f3c3d2]\n", + "└ @ Base loading.jl:1184\n", + "┌ Info: Recompiling stale cache file C:\\Users\\Maxime\\.julia\\compiled\\v1.1\\MetaGraphs\\KfBxe.ji for MetaGraphs [626554b9-1ddb-594c-aa3c-2596fe9399a5]\n", "└ @ Base loading.jl:1184\n" ] } @@ -45,25 +49,13 @@ "outputs": [ { "data": { - "text/latex": [ - "$\\mathsf{G} \\mathsf{F} (a \\land \\mathsf{F} (b \\land \\mathsf{F} c))$" - ], "text/plain": [ - "SpotFormula(PyObject spot.formula(\"GF(a & F(b & Fc))\"))" + "\"GF(a & F(b & Fc))\"" ] }, "execution_count": 2, "metadata": {}, "output_type": "execute_result" - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "┌ Warning: `getindex(o::PyObject, s::AbstractString)` is deprecated in favor of dot overloading (`getproperty`) so elements should now be accessed as e.g. `o.\"s\"` instead of `o[\"s\"]`.\n", - "│ caller = show(::IOContext{Base.GenericIOBuffer{Array{UInt8,1}}}, ::MIME{Symbol(\"text/latex\")}, ::PyCall.PyObject) at PyCall.jl:895\n", - "└ @ PyCall /mnt/c/Users/Maxime/wsl/.julia/packages/PyCall/ttONZ/src/PyCall.jl:895\n" - ] } ], "source": [ @@ -94,152 +86,162 @@ "execution_count": 3, "metadata": {}, "outputs": [ + { + "name": "stderr", + "output_type": "stream", + "text": [ + "┌ Error: mktempdir cleanup\n", + "│ exception = (Base.IOError(\"unlink: resource busy or locked (EBUSY)\", -4082), Union{Ptr{Nothing}, InterpreterIP}[Ptr{Nothing} @0x000000043a2de8d5, Ptr{Nothing} @0x000000043a2af057, Ptr{Nothing} @0x000000050b0f1794, Ptr{Nothing} @0x0000000036188f7b, Ptr{Nothing} @0x0000000036188be0, Ptr{Nothing} @0x000000003618934a, Ptr{Nothing} @0x000000043a2924a5, Ptr{Nothing} @0x000000043a292e25, Ptr{Nothing} @0x000000003618246c, Ptr{Nothing} @0x0000000036182a8d, Ptr{Nothing} @0x0000000036180eb4, Ptr{Nothing} @0x000000043a2924a5, Ptr{Nothing} @0x000000043a293fa6, Ptr{Nothing} @0x000000003617e2f4, Ptr{Nothing} @0x000000043a2924a5, Ptr{Nothing} @0x000000043a293fa6, Ptr{Nothing} @0x000000043a2a0d60, Ptr{Nothing} @0x000000043a2a11d9, Ptr{Nothing} @0x0000000036148347, Ptr{Nothing} @0x000000043a293fa6, Ptr{Nothing} @0x000000043a2a0d60, Ptr{Nothing} @0x000000043a2a11d9, Ptr{Nothing} @0x000000001530f945, Ptr{Nothing} @0x0000000015310627, Ptr{Nothing} @0x000000043a2924a5, Ptr{Nothing} @0x000000043a293fa6, Ptr{Nothing} @0x000000043a2af87e])\n", + "└ @ Base.Filesystem file.jl:587\n" + ] + }, { "data": { "image/svg+xml": [ "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", "\n", - "\n", - " \n", + "\n", + " \n", "\n", "\n", "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", - " \n", - " \n", + " \n", + " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", - "\n", - "\n", + "\n", + "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", - " \n", - " \n", + " \n", + " \n", + " \n", "\n", - "\n", - "\n", + "\n", + "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", - " \n", + " \n", + " \n", "\n", "\n", - " \n", - " \n", - " \n", + " \n", + " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", - " \n", - " \n", + " \n", + " \n", + " \n", "\n", - "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", "\n", - " \n", + " \n", "\n", - "\n", + "\n", "\n", - " \n", + " \n", "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", - " \n", + " \n", "\n", "\n", "\n", "\n" ], "text/plain": [ - "SpotAutomata(PyObject *' at 0x7f6f374c9ba0> >)" + "SpotAutomata(shared_ptr @554793104\n", + ")" ] }, "execution_count": 3, @@ -257,276 +259,285 @@ "execution_count": 4, "metadata": {}, "outputs": [ + { + "name": "stderr", + "output_type": "stream", + "text": [ + "┌ Error: mktempdir cleanup\n", + "│ exception = (Base.IOError(\"unlink: resource busy or locked (EBUSY)\", -4082), Union{Ptr{Nothing}, InterpreterIP}[Ptr{Nothing} @0x000000043a2de8d5, Ptr{Nothing} @0x000000043a2af057, Ptr{Nothing} @0x000000050b0f1794, Ptr{Nothing} @0x0000000036188f7b, Ptr{Nothing} @0x0000000036188be0, Ptr{Nothing} @0x000000003618934a, Ptr{Nothing} @0x000000043a292b96, Ptr{Nothing} @0x000000003618246c, Ptr{Nothing} @0x0000000036182a8d, Ptr{Nothing} @0x0000000036180eb4, Ptr{Nothing} @0x000000043a293fa6, Ptr{Nothing} @0x000000003617e2f4, Ptr{Nothing} @0x000000043a293fa6, Ptr{Nothing} @0x000000043a2a0d60, Ptr{Nothing} @0x000000043a2a11d9, Ptr{Nothing} @0x0000000036148347, Ptr{Nothing} @0x000000043a293fa6, Ptr{Nothing} @0x000000043a2a0d60, Ptr{Nothing} @0x000000043a2a11d9, Ptr{Nothing} @0x000000001530f945, Ptr{Nothing} @0x0000000015310627, Ptr{Nothing} @0x000000043a2924a5, Ptr{Nothing} @0x000000043a293fa6, Ptr{Nothing} @0x000000043a2af87e])\n", + "└ @ Base.Filesystem file.jl:587\n" + ] + }, { "data": { "image/svg+xml": [ "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", - "\n", - "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", "\n", - "\n", - " \n", + "\n", + " \n", "\n", "\n", "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", - " \n", - " \n", + " \n", + " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", - "\n", - "\n", + "\n", + "\n", "\n", - " \n", + " \n", "\n", - "\n", - "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", - "\n", - "\n", "\n", - " \n", + " \n", "\n", + "\n", + "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", - "\n", - "\n", "\n", - " \n", + " \n", "\n", + "\n", + "\n", "\n", - " \n", + " \n", "\n", - "\n", - "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", - "\n", - "\n", "\n", - " \n", + " \n", "\n", + "\n", + "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", - "\n", - "\n", "\n", - " \n", + " \n", "\n", + "\n", + "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", + "\n", + "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", - "\n", - "\n", + "\n", + "\n", "\n", - " \n", + " \n", "\n", + "\n", + "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", - "\n", - "\n", "\n", - " \n", + " \n", "\n", + "\n", + "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", - "\n", - "\n", + "\n", + "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", - "\n", - "\n", + "\n", + "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", - "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", + "\n", + "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", + " \n", "\n", - "\n", - "\n", "\n", - " \n", + " \n", "\n", "\n", - " \n", - "\n", - "\n", - "\n", - "\n", + " \n", "\n", + "\n", + "\n", "\n", - " \n", + " \n", "\n", - "\n", - "\n", + "\n", "\n", - " \n", + " \n", "\n", - "\n", + "\n", "\n", - " \n", + " \n", + "\n", + "\n", + "\n", "\n", - "\n", "\n", - " \n", + " \n", "\n", "\n", "\n", "\n" ], "text/plain": [ - "SpotAutomata(PyObject *' at 0x7f6f374c9c00> >)" + "SpotAutomata(shared_ptr @554790512\n", + ")" ] }, "execution_count": 4, @@ -539,24 +550,292 @@ "surveillance_aut = translate(translator, surveillance)" ] }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "## Deterministic Rabin Automata\n", - "\n", - "Spot.jl provides a Deterministic Rabin Automata structure which is pure Julia. It can be constructed directly from a LTL formula." - ] - }, { "cell_type": "code", "execution_count": 5, "metadata": {}, "outputs": [ + { + "name": "stderr", + "output_type": "stream", + "text": [ + "┌ Error: mktempdir cleanup\n", + "│ exception = (Base.IOError(\"unlink: resource busy or locked (EBUSY)\", -4082), Union{Ptr{Nothing}, InterpreterIP}[Ptr{Nothing} @0x000000043a2de8d5, Ptr{Nothing} @0x000000043a2af057, Ptr{Nothing} @0x000000050b0f1794, Ptr{Nothing} @0x0000000036188f7b, Ptr{Nothing} @0x0000000036188be0, Ptr{Nothing} @0x000000003618934a, Ptr{Nothing} @0x000000043a292b96, Ptr{Nothing} @0x000000003618246c, Ptr{Nothing} @0x0000000036182a8d, Ptr{Nothing} @0x000000043a293fa6, Ptr{Nothing} @0x000000043a4129f5, Ptr{Nothing} @0x000000043a412863, Ptr{Nothing} @0x000000043a4132d0, Ptr{Nothing} @0x000000043a4139aa, InterpreterIP(CodeInfo(\n", + "\u001b[90m1 ─\u001b[39m %1 = plot_automata(surveillance_aut)\n", + "\u001b[90m└──\u001b[39m return %1\n", + "), 0x0000000000000000), Ptr{Nothing} @0x000000043a2c874e, Ptr{Nothing} @0x000000043a2c93b1, Ptr{Nothing} @0x000000003614978a, Ptr{Nothing} @0x0000000036147a2f, Ptr{Nothing} @0x000000043a293fa6, Ptr{Nothing} @0x000000043a2a0d60, Ptr{Nothing} @0x000000043a2a11d9, Ptr{Nothing} @0x000000001530f945, Ptr{Nothing} @0x0000000015310627, Ptr{Nothing} @0x000000043a2924a5, Ptr{Nothing} @0x000000043a293fa6, Ptr{Nothing} @0x000000043a2af87e])\n", + "└ @ Base.Filesystem file.jl:587\n" + ] + }, { "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + " \n", + "\n", + "\n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + " \n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + "\n", + "\n", + " \n", + "\n", + "\n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + " \n", + "\n", + "\n", + "\n", + "\n", + " \n", + "\n", + "\n", + "\n", + " \n", + "\n", + "\n", + "\n", + " \n", + "\n", + "\n", + "\n", + "\n", + "\n", + " \n", + "\n", + "\n", + "\n", + "\n" + ], "text/plain": [ - "4" + "TikzPictures.TikzPicture(\"\\r\\n\\\\begin{tikzpicture}[>=latex,line join=bevel,]\\r\\n \\\\pgfsetlinewidth{1bp}\\r\\n%%\\r\\n\\\\begin{scope}\\r\\n \\\\definecolor{strokecol}{rgb}{0.0,0.0,0.0};\\r\\n \\\\pgfsetstrokecolor{strokecol}\\r\\n \\\\draw (242.0bp,237.09bp) node {\\$[Büchi]\\$};\\r\\n\\\\end{scope}\\r\\n \\\\pgfsetcolor{black}\\r\\n % Edge: 0 -> 3\\r\\n \\\\draw [->] (77.491bp,69.658bp) .. controls (84.099bp,64.774bp) and (92.03bp,59.73bp) .. (100.0bp,56.595bp) .. controls (218.41bp,10.015bp) and (375.19bp,23.508bp) .. (447.84bp,32.931bp);\\r\\n \\\\definecolor{strokecol}{rgb}{0.0,0.0,0.0};\\r\\n \\\\pgfsetstrokecolor{strokecol}\\r\\n \\\\draw (262.5bp,35.095bp) node {\\$a \\\\land b \\\\land \\\\lnot c\\$};\\r\\n % Edge: 1 -> 0\\r\\n \\\\draw [->] (180.4bp,154.95bp) .. controls (173.99bp,149.7bp) and (165.95bp,143.77bp) .. (158.0bp,139.59bp) .. controls (133.98bp,126.99bp) and (123.3bp,134.49bp) .. (100.0bp,120.59bp) .. controls (93.861bp,116.93bp) and (87.904bp,112.15bp) .. (75.252bp,100.09bp);\\r\\n \\\\draw (129.0bp,147.09bp) node {\\$a \\\\land b \\\\land c\\$};\\r\\n % Edge: 2 -> 3\\r\\n \\\\draw [->] (361.26bp,67.45bp) .. controls (381.31bp,61.292bp) and (415.13bp,50.908bp) .. (448.39bp,40.696bp);\\r\\n \\\\draw (411.5bp,64.095bp) node {\\$a \\\\land \\\\lnot c\\$};\\r\\n % Edge: 0 -> 2\\r\\n \\\\draw [->] (82.158bp,82.768bp) .. controls (132.5bp,80.801bp) and (259.39bp,75.842bp) .. (325.51bp,73.259bp);\\r\\n \\\\draw (194.5bp,86.095bp) node {\\$ \\\\lnot a \\\\land b\\$};\\r\\n % Edge: 2 -> 2\\r\\n \\\\draw [->] (332.26bp,87.011bp) .. controls (328.33bp,97.761bp) and (332.08bp,108.59bp) .. (343.5bp,108.59bp) .. controls (351.17bp,108.59bp) and (355.38bp,103.7bp) .. (354.74bp,87.011bp);\\r\\n \\\\draw (343.5bp,116.09bp) node {\\$ \\\\lnot a\\$};\\r\\n % Edge: 2 -> 0\\r\\n \\\\draw [->] (325.46bp,69.016bp) .. controls (295.29bp,63.16bp) and (230.51bp,52.738bp) .. (176.0bp,58.595bp) .. controls (146.93bp,61.718bp) and (114.43bp,69.16bp) .. (81.556bp,77.729bp);\\r\\n \\\\draw (194.5bp,66.095bp) node {\\$a \\\\land c\\$};\\r\\n % Edge: 3 -> 0\\r\\n \\\\draw [->] (448.81bp,29.32bp) .. controls (442.95bp,27.245bp) and (436.25bp,25.088bp) .. (430.0bp,23.595bp) .. controls (343.59bp,2.946bp) and (319.25bp,-5.7046bp) .. (231.0bp,4.5947bp) .. controls (171.57bp,11.53bp) and (150.68bp,3.7923bp) .. (100.0bp,35.595bp) .. controls (91.584bp,40.876bp) and (84.157bp,48.61bp) .. (72.092bp,64.596bp);\\r\\n \\\\draw (262.5bp,12.095bp) node {\\$c\\$};\\r\\n % Edge: 1 -> 3\\r\\n \\\\draw [->] (212.53bp,167.3bp) .. controls (246.22bp,167.89bp) and (322.63bp,165.2bp) .. (375.0bp,132.59bp) .. controls (405.99bp,113.3bp) and (433.18bp,80.584bp) .. (455.19bp,50.387bp);\\r\\n \\\\draw (343.5bp,164.09bp) node {\\$a \\\\land b \\\\land \\\\lnot c\\$};\\r\\n % Edge: 1 -> 1\\r\\n \\\\draw [->] (183.79bp,181.39bp) .. controls (180.31bp,192.01bp) and (183.88bp,202.59bp) .. (194.5bp,202.59bp) .. controls (201.64bp,202.59bp) and (205.59bp,197.82bp) .. (205.21bp,181.39bp);\\r\\n \\\\draw (194.5bp,210.09bp) node {\\$ \\\\lnot b\\$};\\r\\n % Edge: 1 -> 2\\r\\n \\\\draw [->] (209.57bp,156.43bp) .. controls (215.92bp,152.13bp) and (223.64bp,147.26bp) .. (231.0bp,143.59bp) .. controls (257.68bp,130.3bp) and (268.83bp,136.56bp) .. (294.0bp,120.59bp) .. controls (305.3bp,113.43bp) and (316.06bp,103.25bp) .. (331.42bp,86.435bp);\\r\\n \\\\draw (262.5bp,151.09bp) node {\\$ \\\\lnot a \\\\land b\\$};\\r\\n % Edge: 3 -> 3\\r\\n \\\\draw [->] (456.77bp,51.136bp) .. controls (454.17bp,61.503bp) and (457.25bp,71.595bp) .. (466.0bp,71.595bp) .. controls (471.74bp,71.595bp) and (475.04bp,67.249bp) .. (475.23bp,51.136bp);\\r\\n \\\\draw (466.0bp,79.095bp) node {\\$ \\\\lnot c\\$};\\r\\n % Edge: I -> 0\\r\\n \\\\draw [->] (1.1664bp,83.595bp) .. controls (2.7183bp,83.595bp) and (14.889bp,83.595bp) .. (37.856bp,83.595bp);\\r\\n % Edge: 0 -> 1\\r\\n \\\\draw [->] (65.997bp,104.89bp) .. controls (71.309bp,122.41bp) and (81.565bp,146.3bp) .. (100.0bp,158.59bp) .. controls (119.53bp,171.62bp) and (146.7bp,172.52bp) .. (176.73bp,169.7bp);\\r\\n \\\\draw (129.0bp,178.09bp) node {\\$ \\\\lnot b\\$};\\r\\n % Edge: 0 -> 0\\r\\n \\\\draw [->] (52.683bp,104.59bp) .. controls (51.78bp,114.68bp) and (54.219bp,123.59bp) .. (60.0bp,123.59bp) .. controls (63.704bp,123.59bp) and (66.036bp,119.94bp) .. (67.317bp,104.59bp);\\r\\n \\\\draw (60.0bp,131.09bp) node {\\$a \\\\land b \\\\land c\\$};\\r\\n % Node: 0\\r\\n\\\\begin{scope}\\r\\n \\\\definecolor{strokecol}{rgb}{0.0,0.0,0.0};\\r\\n \\\\pgfsetstrokecolor{strokecol}\\r\\n \\\\draw (60.0bp,83.59bp) ellipse (18.0bp and 18.0bp);\\r\\n \\\\draw (60.0bp,83.59bp) ellipse (22.0bp and 22.0bp);\\r\\n \\\\draw (60.0bp,83.595bp) node {\\$0\\$};\\r\\n\\\\end{scope}\\r\\n % Node: 2\\r\\n\\\\begin{scope}\\r\\n \\\\definecolor{strokecol}{rgb}{0.0,0.0,0.0};\\r\\n \\\\pgfsetstrokecolor{strokecol}\\r\\n \\\\draw (343.5bp,72.59bp) ellipse (18.0bp and 18.0bp);\\r\\n \\\\draw (343.5bp,72.595bp) node {\\$2\\$};\\r\\n\\\\end{scope}\\r\\n % Node: 1\\r\\n\\\\begin{scope}\\r\\n \\\\definecolor{strokecol}{rgb}{0.0,0.0,0.0};\\r\\n \\\\pgfsetstrokecolor{strokecol}\\r\\n \\\\draw (194.5bp,166.59bp) ellipse (18.0bp and 18.0bp);\\r\\n \\\\draw (194.5bp,166.59bp) node {\\$1\\$};\\r\\n\\\\end{scope}\\r\\n % Node: 3\\r\\n\\\\begin{scope}\\r\\n \\\\definecolor{strokecol}{rgb}{0.0,0.0,0.0};\\r\\n \\\\pgfsetstrokecolor{strokecol}\\r\\n \\\\draw (466.0bp,35.59bp) ellipse (18.0bp and 18.0bp);\\r\\n \\\\draw (466.0bp,35.595bp) node {\\$3\\$};\\r\\n\\\\end{scope}\\r\\n%\\r\\n\\\\end{tikzpicture}\\r\\n\", \"\", \"\\n\\\\usepackage{amsmath,amsfonts,amssymb}\\n\\\\usetikzlibrary{snakes,arrows,shapes}\", true)" ] }, "execution_count": 5, @@ -565,8 +844,26 @@ } ], "source": [ - "dra = DeterministicRabinAutomata(surveillance)\n", - "nextstate(dra, 4, (:a,:b,:c))" + "plot_automata(surveillance_aut)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## Deterministic Rabin Automata\n", + "\n", + "Spot.jl provides a Deterministic Rabin Automata structure which is pure Julia. It can be constructed directly from a LTL formula." + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "metadata": {}, + "outputs": [], + "source": [ + "# dra = DeterministicRabinAutomata(surveillance)\n", + "# nextstate(dra, 4, (:a,:b,:c))" ] } ], diff --git a/src/Spot.jl b/src/Spot.jl index 4c99d13..f13b9ef 100755 --- a/src/Spot.jl +++ b/src/Spot.jl @@ -1,67 +1,90 @@ -module Spot - -# Package code goes here. -using PyCall -using Parameters -using LightGraphs -using MetaGraphs -using TikzPictures - -const spot = PyNULL() - -function __init__() - pyversion = PyCall.pyversion - pythonspot = "../deps/spot/lib/python"*string(pyversion.major)*"."*string(pyversion.minor)*"/site-packages/" - pushfirst!(PyVector(pyimport("sys").path),joinpath(dirname(@__FILE__), pythonspot)) - # global spot = pyimport("spot") - copy!(spot, pyimport("spot")) - spot.setup() # for display style -end - -export - spot - -export - SpotFormula, - is_ltl_formula, - to_str, - is_eventual, - is_sugar_free_ltl, - is_literal, - is_boolean, - atomic_prop_collect, - is_reachability, - is_constrained_reachability, - @ltl_str - -include("formulas.jl") - -export - AbstractAutomata, - SpotAutomata, - num_states, - num_edges, - get_init_state_number, - get_edges_labels, - atomic_propositions, - label_to_function, - label_to_array, - get_rabin_acceptance, - to_generalized_rabin, - is_deterministic - -include("automata.jl") - -export - LTLTranslator, - translate - -include("translator.jl") - -export - DeterministicRabinAutomata, - nextstate - -include("rabin_automata.jl") - +__precompile__(false) +module Spot + +using Cxx +using Libdl +using Parameters +using TikzPictures +using LightGraphs +using MetaGraphs + + +const depfile = joinpath(@__DIR__, "..", "deps", "deps.jl") +if isfile(depfile) + include(depfile) +else + error("libspot not properly installed. Please run Pkg.build(\"Spot\")") +end + +const path_to_header = joinpath(@__DIR__, "..", "deps", "usr", "include") + +function __init__() + addHeaderDir(path_to_header, kind=C_System) + Libdl.dlopen(libspot, Libdl.RTLD_GLOBAL) + + cxx"#include " + cxx"#include " + cxx"#include " + + # formula + cxx"#include " + cxx"#include " + cxx"#include " + cxx"#include " + + # automata + cxx"#include " + cxx"#include " + cxx"#include " + cxx"#include " + cxx"#include " + cxx"#include " + cxx"#include " +end + +export + SpotFormula, + is_ltl_formula, + to_str, + is_eventual, + is_sugar_free_ltl, + is_literal, + is_boolean, + atomic_prop_collect, + is_reachability, + is_constrained_reachability, + @ltl_str + +include("formulas.jl") + +export + AbstractAutomata, + SpotAutomata, + num_states, + num_edges, + get_init_state_number, + is_deterministic, + to_generalized_rabin, + split_edges, + atomic_propositions, + get_edges, + get_labels, + label_to_array, + get_rabin_acceptance, + plot_automata + +include("automata.jl") + +export + LTLTranslator, + translate + +include("translator.jl") + +export + DeterministicRabinAutomata, + nextstate + +include("rabin_automata.jl") + end # module spot \ No newline at end of file diff --git a/src/automata.jl b/src/automata.jl index 2560bc5..33de845 100755 --- a/src/automata.jl +++ b/src/automata.jl @@ -3,71 +3,94 @@ abstract type AbstractAutomata end struct SpotAutomata <: AbstractAutomata - a::PyObject + a::Cxx.CxxCore.CppValue end -function SpotAutomata(a::PyObject, split::Bool) - if split - return SpotAutomata(spot.split_edges(a)) - else - return SpotAutomata(a) - end +""" + split_edges(aut::SpotAutomata) +add dummy edges +""" +function split_edges(aut::SpotAutomata) + return SpotAutomata(@cxx spot::split_edges(aut.a)) end function num_states(aut::SpotAutomata) - return aut.a.num_states() + return convert(Int64, icxx"""$(aut.a)->num_states();""") end function get_init_state_number(aut::SpotAutomata) - return aut.a.get_init_state_number() + 1 + return convert(Int64, icxx"""$(aut.a)->get_init_state_number();""") + 1 end function num_edges(aut::SpotAutomata) - return aut.a.num_edges() + return convert(Int64, icxx"""$(aut.a)->num_edges();""") end function atomic_propositions(aut::SpotAutomata) - return [Symbol(a.to_str()) for a in aut.a.ap()] + aps = icxx"""$(aut.a)->ap();""" + return [Symbol(SpotFormula(ap)) for ap in aps] end function to_generalized_rabin(aut::SpotAutomata, split=true) - return SpotAutomata(spot.to_generalized_rabin(aut.a), split) + gra = SpotAutomata(@cxx spot::to_generalized_rabin(aut.a)) + if split + return split_edges(gra) + end + return gra end function is_deterministic(aut::SpotAutomata) - return aut.a.is_deterministic() + return icxx"""spot::is_deterministic($(aut.a));""" end """ - get_edges_labels(aut::SpotAutomata) -returns a list of edges as pairs (src, dest) and their associated labels as a SpotFormula. -The edges are labeled by a conjunction of all the atomic proposition. -See spot.split_edges documentation for more information. -This is inspired from https://spot.lrde.epita.fr/tut24.html + edges(aut::SpotAutomata) + +returns a list of edges as pairs (src, dest) """ -function get_edges_labels(aut::SpotAutomata) - bdict = aut.a.get_dict() - edges = Tuple{Int64, Int64}[] - labels = SpotFormula[] - for e in aut.a.edges() - push!(edges, (e.src + 1, e.dst + 1)) - push!(labels, ((SpotFormula(spot.bdd_to_formula(e.cond, bdict))))) +function get_edges(aut::SpotAutomata) + cpp_edges = icxx""" + std::vector> edge_list; + for (auto& e: $(aut.a)->edges()) + { + std::vector edge; + edge.push_back(e.src); + edge.push_back(e.dst); + edge_list.push_back(edge); + } + edge_list; + """ + + edges = Vector{Tuple{Int64, Int64}}(undef, length(cpp_edges)) + for (i, e) in enumerate(cpp_edges) + edges[i] = (e[0] + 1, e[1] + 1) # this is a cpp vector, so it is 0 index! end - return edges, labels + return edges end """ - label_to_function(ap::Vector{Symbol}, label::String) -returns a functions with atomic propositions as arguments. -The function evaluates the boolean expression represented in the label. + get_edges_labels(aut::SpotAutomata) +returns a list of all the edges labels as a SpotFormula. +The edges are labeled by a conjunction of all the atomic proposition. +See spot.split_edges documentation for more information. +This is inspired from https://spot.lrde.epita.fr/tut24.html """ -function label_to_function(ap::Vector{Symbol}, label::String) - parsed_formula = Meta.parse(label) - fun_args = Expr(:tuple, ap...) - ex = Expr(:->, fun_args, parsed_formula) - return eval(ex) +function get_labels(aut::SpotAutomata) + cpp_labs = icxx""" + std::vector labs_list; + auto bdict = $(aut.a)->get_dict(); + for (auto& e: $(aut.a)->edges()) + { + spot::formula f = spot::bdd_to_formula(e.cond, bdict); + labs_list.push_back(f); + } + labs_list; + """ + return [SpotFormula(f) for f in cpp_labs] end +const TRUE_CONSTANT = :true_constant + """ label_to_array(lab::SpotFormula) convert a conjunction into an array of symbols. @@ -76,39 +99,53 @@ The outputs is the list of AP that are true in the input formula function label_to_array(lab::SpotFormula) @assert is_boolean(lab) positive_ap = Symbol[] - if length(lab.f) <= 1 - if lab.f.is_tt() - push!(positive_ap, Symbol(:true_constant)) - elseif !lab.f._is(spot.op_Not) - push!(positive_ap, Symbol(lab.f.ap_name())) + if length(lab) <= 1 + if @cxx lab.f->is_tt() + push!(positive_ap, TRUE_CONSTANT) + elseif !( @cxx lab.f->is(spot::op::Not) ) + push!(positive_ap, Symbol(lab)) else return positive_ap end end - for ap in lab.f - if !ap._is(spot.op_Not) - push!(positive_ap, Symbol(ap.ap_name())) - end + cpp_aps = icxx""" + std::vector positive_aps; + for (auto ap: $(lab.f)) { + if ( !ap.is(spot::op::Not) ){ + positive_aps.push_back(ap); + } + } + positive_aps; + """ + for ap in cpp_aps + push!(positive_ap, Symbol(SpotFormula(ap))) end return positive_ap end """ + get_rabin_acceptance(aut::SpotAutomata) Return a Rabin acceptance condition as a list of pairs (Fin, Inf) where Fin is a set of states to be visited finitely often and Inf inifinitely often """ function get_rabin_acceptance(aut::SpotAutomata) - acc = aut.a.acc() - israbin, acc_sets = acc.is_rabin_like() - @assert israbin "SpotError: automata is not Rabin like" - fin_inf_sets = Vector{Tuple{Set{Int64}, Set{Int64}}}(undef, length(acc_sets)) - for (i,s) in enumerate(acc_sets) + acc = icxx"$(aut.a)->acc();" + rabin_pairs = icxx""" + std::vector pairs; + $acc.is_rabin_like(pairs); + pairs; + """ + @assert !isempty(rabin_pairs) "SpotError: automata is not Rabin like" + fin_inf_sets = Vector{Tuple{Set{Int64}, Set{Int64}}}(undef, length(rabin_pairs)) + for (i,s) in enumerate(rabin_pairs) stateinfset = Set{Int64}() statefinset = Set{Int64}() - infset = Set(collect(s.inf.sets())) - finset = Set(collect(s.fin.sets())) - for state in 1:aut.a.num_states() - stateset = Set(collect(aut.a.state_acc_sets(state - 1).sets())) + infset = convert(Set{Int64}, icxx"$s.inf.sets();") + finset = convert(Set{Int64}, icxx"$s.fin.sets();") + + + for state in 1:num_states(aut) + stateset = convert(Set{Int64}, icxx"$(aut.a)->state_acc_sets($state - 1).sets();") if !isempty(intersect(infset,stateset)) push!(stateinfset, state) elseif !isempty(intersect(finset, stateset)) @@ -120,35 +157,38 @@ function get_rabin_acceptance(aut::SpotAutomata) return fin_inf_sets end -""" - get_inf_fin_sets(aut::SpotAutomata) -Given a SpotAutomata, parse the accepting condition and returns - the set of states that must be visited infinitely often (inf_set) - and the set of states that must be visited finitely often (fin_set) -""" -function get_inf_fin_sets(aut::SpotAutomata) - inf_set=Set{Int64}() - fin_set =Set{Int64}() - l = aut.a.get_acceptance().__str__() #XXX hack - inf_set = Set{Int64}() - for m in eachmatch(r"Inf\(\d+\)", l) - push!(inf_set, parse(Int64, match(r"\d+",m.match).match)) - end - fin_set = Set{Int64}() - for m in eachmatch(r"Fin\(\d+\)", l) - push!(fin_set, parse(Int64, match(r"\d+",m.match).match)) - end - return (inf_set, fin_set) +const AccCond = Cxx.CxxCore.CppRef{Cxx.CxxCore.CppBaseType{Symbol("spot::acc_cond")},(false, false, false)} + +function is_rabin_like(acc::AccCond) + rabin = icxx""" + std::vector pairs; + $acc.is_rabin_like(pairs); + """ + return convert(Bool, rabin) +end + +const MarkContainer = Cxx.CxxCore.CppValue{Cxx.CxxCore.CxxQualType{Cxx.CxxCore.CppBaseType{Symbol("spot::internal::mark_container")},(false, false, false)},4} + +function Base.convert(::typeof(Set{Int64}), mc::MarkContainer) + v = icxx""" + std::vector vec; + for (unsigned int s: $mc){ + vec.push_back(s); + } + vec; + """ + return Set(collect(Int64, v)) end ## Rendering -function plot(aut::SpotAutomata) - autdot = aut.a.to_str(format="dot"); +function plot_automata(aut::SpotAutomata) texstr = mktempdir() do path dotfile = joinpath(path, "graph.dot") open(dotfile, "w") do f - write(f, autdot) + redirect_stdout(f) do + icxx"spot::print_dot(std::cout, $(aut.a));" + end end xdotfile = joinpath(path, "graph.xdot") run(pipeline(`dot -Txdot $dotfile `, stdout=xdotfile)) @@ -170,5 +210,5 @@ function plot(aut::SpotAutomata) end function Base.show(f::IO, a::MIME"image/svg+xml", aut::SpotAutomata) - show(f, a, plot(aut)) + show(f, a, plot_automata(aut)) end \ No newline at end of file diff --git a/src/formulas.jl b/src/formulas.jl index 11b9c2d..11f215f 100755 --- a/src/formulas.jl +++ b/src/formulas.jl @@ -1,5 +1,5 @@ struct SpotFormula - f::PyObject + f::Cxx.CxxCore.CppValue end macro ltl_str(l) @@ -7,48 +7,48 @@ macro ltl_str(l) end function SpotFormula(f::AbstractString) - return SpotFormula(spot.formula(f)) + return SpotFormula(@cxx spot::parse_formula(pointer(f))) end """ is_ltl_formula(f::SpotFormula) return true if the formula is a Linear Temporal Logic formula """ -is_ltl_formula(f::SpotFormula) = f.f.is_ltl_formula() - -to_str(f::SpotFormula) = f.f.to_str() -Base.string(f::SpotFormula) = f.f.to_str() +is_ltl_formula(f::SpotFormula) = @cxx f.f -> is_ltl_formula() """ is_eventual(f::SpotFormula) Whether the formula is purely eventual. """ -is_eventual(f::SpotFormula) = f.f.is_eventual() +is_eventual(f::SpotFormula) = @cxx f.f -> is_eventual() """ is_sugar_free_ltl(f::SpotFormula) Whether the formula avoids the F and G operators. """ -is_sugar_free_ltl(f::SpotFormula) = f.f.is_sugar_free_ltl() +is_sugar_free_ltl(f::SpotFormula) = @cxx f.f -> is_sugar_free_ltl() """ is_literal() Whether the formula is an atomic proposition or its negation. """ -is_literal(f::SpotFormula) = f.f.is_literal() +is_literal(f::SpotFormula) = @cxx f.f -> is_literal() """ is_boolean() Whether the formula is boolean """ -is_boolean(f::SpotFormula) = f.f.is_boolean() +is_boolean(f::SpotFormula) = @cxx f.f -> is_boolean() """ is_reachability(f::SpotFormula) returns true if a formula is of type `F a` """ function is_reachability(f::SpotFormula) - return f.f._is(spot.op_F) && get(f.f, 0).is_boolean() + return icxx""" + spot::formula ff = $(f.f); + ff.is(spot::op::F) && ff[0].is_boolean(); + """ end """ @@ -56,13 +56,43 @@ end returns true if a formula is of type `a U b` """ function is_constrained_reachability(f::SpotFormula) - return f.f._is(spot.op_U) && get(f.f, PyObject, 0).is_boolean() && get(f.f, PyObject, 1).is_boolean() + return icxx""" + spot::formula ff = $(f.f); + ff.is(spot::op::U) && ff[0].is_boolean() && ff[1].is_boolean(); + """ end """ atomic_prop_collect(f::SpotFormula) returns the list of atomic propositions in f """ -atomic_prop_collect(f::SpotFormula) = [Symbol(ap.to_str()) for ap in spot.atomic_prop_collect(f.f)] +function atomic_prop_collect(f::SpotFormula) + sap = @cxx spot::atomic_prop_collect(f.f) + vap = icxx""" + std::vector v($sap->begin(), $sap->end()); + v; + """ + return [Symbol(SpotFormula(ap)) for ap in vap] +end + +""" + Base.length(f::SpotFormula) + +Returns the number of children in the formula AST +""" +function Base.length(f::SpotFormula) + return convert(Int64, @cxx f.f->size()) +end + +## Rendering and conversion + +Base.string(f::SpotFormula) = String(@cxx spot::str_psl(f.f)) +Base.Symbol(f::SpotFormula) = Symbol(string(f)) + +function Base.show(io::IO, m::MIME{Symbol("text/latex")}, f::SpotFormula) + show(io, m, latexstring(String(@cxx spot::str_latex_psl(f.f)))) +end -Base.show(io::IO, m::MIME{Symbol("text/latex")}, f::SpotFormula) = show(io, m, f.f) \ No newline at end of file +function Base.show(io::IO, mime::MIME"text/plain", f::SpotFormula) + show(io, mime, string(f)) +end \ No newline at end of file diff --git a/src/rabin_automata.jl b/src/rabin_automata.jl index 9a26994..d00203a 100755 --- a/src/rabin_automata.jl +++ b/src/rabin_automata.jl @@ -18,13 +18,15 @@ end # extract a Rabin Automata from an LTL formula using Spot.jl function DeterministicRabinAutomata(ltl::SpotFormula, translator::LTLTranslator = LTLTranslator(deterministic=true, buchi=true, state_based_acceptance=true)) - dra = SpotAutomata(translate(translator, ltl).a, true) # split edges - # dra = to_generalized_rabin(aut) # unclear if needed + aut = translate(translator, ltl) + dra = to_generalized_rabin(aut) # unclear if needed + dra = split_edges(dra) @assert is_deterministic(dra) states = 1:num_states(dra) initial_state = get_init_state_number(dra) APs = atomic_propositions(dra) - edgelist, labels = get_edges_labels(dra) + edgelist = get_edges(dra) + labels = get_labels(dra) sdg = SimpleDiGraph(num_states(dra)) for e in edgelist add_edge!(sdg, e) @@ -52,7 +54,7 @@ get_rabin_acceptance(aut::DeterministicRabinAutomata) = aut.acc_sets function nextstate(dra::DeterministicRabinAutomata, q::Int64, lab::NTuple{N,Symbol}) where N next_states = neighbors(dra.transition, q) edge_it = filter_edges(dra.transition, - (g, e) -> (src(e) == q) && (lab ∈ props(g, e)[:cond] || (:true_constant,) ∈ props(g, e)[:cond])) + (g, e) -> (src(e) == q) && (lab ∈ props(g, e)[:cond] || (TRUE_CONSTANT,) ∈ props(g, e)[:cond])) edge_list = collect(edge_it) if isempty(edge_list) return nothing diff --git a/src/translator.jl b/src/translator.jl index ebb40ad..4de29c3 100755 --- a/src/translator.jl +++ b/src/translator.jl @@ -29,16 +29,64 @@ end translate(translator::LTLTranslator, ltl::string) translate an LTL formula into an automata -Options are set using the translator object. More options can be passed as strings. +Options are set using the translator object. See https://spot.lrde.epita.fr/ltl2tgba.html for extra options that are not in LTLTranslator """ -function translate(translator::LTLTranslator, ltl::SpotFormula, args...) - options = String[] - translator.buchi ? push!(options, "BA") : nothing - translator.monitor ? push!(options, "monitor") : nothing - translator.deterministic ? push!(options, "deterministic") : nothing - translator.generic ? push!(options, "generic") : nothing - translator.parity ? push!(options, "parity") : nothing - translator.state_based_acceptance ? push!(options, "sbacc") : nothing - return SpotAutomata(spot.translate(ltl.f, options..., args...)) +function translate(translator::LTLTranslator, ltl::SpotFormula) + trans = @cxxnew spot::translator() + if translator.tgba + autom_type = @cxx spot::postprocessor::TGBA + @cxx trans -> set_type(autom_type) + end + if translator.buchi + autom_type = @cxx spot::postprocessor::BA + @cxx trans -> set_type(autom_type) + end + if translator.monitor + autom_type = @cxx spot::postprocessor::Monitor + @cxx trans -> set_type(autom_type) + end + if translator.deterministic + autom_pref = @cxx spot::postprocessor::Deterministic + @cxx trans -> set_pref(autom_pref) + end + if translator.generic + autom_type = @cxx spot::postprocessor::Generic + @cxx trans -> set_type(autom_type) + end + if translator.parity + autom_type = @cxx spot::postprocessor::Parity + @cxx trans -> set_type(autom_type) + end + if translator.state_based_acceptance + autom_pref = @cxx spot::postprocessor::SBAcc + @cxx trans -> set_pref(autom_pref) + end + aut = @cxx trans->run(ltl.f) + return SpotAutomata(aut) + # aut = icxx""" + # spot::translator trans; + # if ($(translator.buchi)){ + # trans.set_type(spot::postprocessor::BA); + # } + # else if ($(translator.generic)){ + # trans.set_type(spot::postprocessor::Generic); + # } + # else if ($(translator.parity)){ + # trans.set_type(spot::postprocessor::Parity); + # } + # else if ($(translator.monitor)){ + # trans.set_type(spot::postprocessor::Monitor); + # } + + # if ($(translator.deterministic)){ + # trans.set_pref(spot::postprocessor::Deterministic); + # } + # else if ($(translator.state_based_acceptance)){ + # trans.set_pref(spot::postprocessor::SBAcc); + # } + # spot::twa_graph_ptr aut = trans.run($(ltl.f)); + # aut; + # """ + return SpotAutomata(aut) end \ No newline at end of file diff --git a/test/automata.jl b/test/automata.jl new file mode 100644 index 0000000..a0cd6ff --- /dev/null +++ b/test/automata.jl @@ -0,0 +1,264 @@ +abstract type Automata{Q, A} end + +# interface for automata: + +struct BuchiAutomata{Q, A} <: Automata{Q, A} + states::Vector{Q} + alphabet::Vector{A} + transition::Dict{Tuple{Int64, Set{A}}, Int64} # use custom struct for transitions? + initialstate::Q + acceptance::Set{Q} + property::String +end + +struct RabinAutomata{Q, A} <: Automata{Q, A} + states::Vector{Q} + alphabet::Vector{A} + transition::Dict{Tuple{Int64, Set{A}}, Int64} # use custom struct for transitions? + initialstate::Q + inf::Set{Q} # states that must be visited infinitely often + fin::Set{Q} # states that must be visited finitely often + property::String +end + +function acceptance_condition(automata::BuchiAutomata{Q, A}) where {Q, A} + return automata.acceptance, Q[] +end + +function acceptance_condition(automata::RabinAutomata) + return automata.inf, automata.fin +end + +function POMDPs.stateindex(autom::B, q::Int64) where B <: Automata + return q +end + +function POMDPs.n_states(autom::Union{BuchiAutomata, RabinAutomata}) + return length(autom.states) +end + +# return true if there is a transitions q, l, q' given q and l +function has_transition(automata::Automata{Q, String}, q::Q, word::Vector{String}) where Q + set_word = Set(word) + if haskey(automata.transition, (q, set_word)) + return true + else + for w in word + if haskey(automata.transition, (q, w)) + return true + end + end + end + return false +end + +# will return a key error if no transition exists! +function POMDPs.transition(automata::Automata{Q, String}, q::Q, word::Vector{String}) where Q + set_word = Set(word) + if haskey(automata.transition, (q, set_word)) + return automata.transition[(q, set_word)] + else + for w in word + if haskey(automata.transition, (q, w)) + return automata.transition[(q,w)] + end + end + end + return throw("AutomataTransitionError: No transition for state $q, input word $word") +end + +# FILE PARSER + +# convert LTL formula to automata +function ltl2tgba(property::String, automata_file::String="automata.hoa") + run(`ltl2tgba -G -D -S -H -f $property -o $automata_file`) +end + + +# parse a .hoa file to return a BuchiAutomata +# only support Buchi! +function hoa2buchi(file_name::String) + # initialize properties + property = "" + n_states = 0 + states = Vector{Int64}() + initialstate = 0 + alphabet = Vector{String}() + n_inputs = 0 + transition = Dict{Tuple{Int64, Set{String}}, Int64}() + acceptance = Set{Int64}() + + open(file_name, "r") do f + # parse header first + ln = 1 + l = readline(f) + while l != "--BODY--" + # parse header + if occursin("acc-name", l) + if !occursin("Buchi", l) + autom_type = l[length("acc-name: ")+1:end] + throw("HOAParsingError: this function only supports Buchi automata, the file you provided was for a $autom_type") + end + elseif occursin("States", l) + n_states = parse(Int64, match(r"\d+", l).match) + states = 1:n_states + elseif occursin("Start", l) + initialstate = parse(Int64, match(r"\d+", l).match) + 1 + elseif occursin(l, "name") + name = match(r"\"(.*?)\"", l).match + property = name[2:end-1] # remove quotes + elseif occursin("AP", l) + alphabet = parse_alphabet(l) + elseif occursin("Acceptance", l) + + end + l = readline(f) + ln += 1 + end + # parse body + l = readline(f) + ln += 1 + cur_state = 0 + while l != "--END--" + if occursin("State", l) + # set current state + cur_state = parse(Int64, match(r"\d+", l).match) + 1 + # check if it is accepting + acc = match(r"\{(.*?)\}", l) + if acc != nothing + push!(acceptance, cur_state) + end + else + # set edge + input = match(r"\[(.*?)\]", l).match[2:end-1] + inputs = split(input, "&") + for i=1:length(inputs) + inputs[i] = replace(inputs[i], r"\d+" => x->alphabet[parse(Int64, x)+1]) + end + inputs = Set(inputs) + succ = parse(Int64, match(r"\s(.*?)($|\s)", l).match) + 1 + transition[(cur_state, inputs)] = succ + end + l = readline(f) + ln += 1 + end + end + return BuchiAutomata{Int64, String}(states, alphabet, transition, initialstate, acceptance, property) +end + +function hoa2rabin(file_name::String) + # initialize properties + property = "" + n_states = 0 + states = Vector{Int64}() + initialstate = 0 + alphabet = Vector{String}() + n_inputs = 0 + transition = Dict{Tuple{Int64, Set{String}}, Int64}() + fin = Set{Int64}() + inf = Set{Int64}() + fin_idx = 1 + inf_idx = 0 + + open(file_name, "r") do f + # parse header first + ln = 1 + l = readline(f) + while l != "--BODY--" + # parse header + if occursin("acc-name", l) + if !occursin("Rabin", l) + autom_type = l[length("acc-name: ")+1:end] + throw("HOAParsingError: this function only supports Rabin automata, the file you provided was for a $autom_type") + end + elseif occursin("States", l) + n_states = parse(Int64, match(r"\d+", l).match) + states = 1:n_states + elseif occursin("Start", l) + initialstate = parse(Int64, match(r"\d+", l).match) + 1 + elseif occursin("name", l) + name = match(r"\"(.*?)\"", l).match + property = name[2:end-1] # remove quotes + elseif occursin("AP", l) + alphabet = parse_alphabet(l) + elseif occursin("Acceptance", l) + n_sets = parse(Int64, match(r"\d+", l).match) + @assert n_sets == 2 + fin_str = match(r"Fin\(\d+\)", l).match + fin_idx = parse(Int64, match(r"\d+", fin_str).match) + inf_str = match(r"Inf\(\d+\)", l).match + inf_idx = parse(Int64, match(r"\d+", inf_str).match) + end + l = readline(f) + ln += 1 + end + # parse body + l = readline(f) + ln += 1 + cur_state = 0 + while l != "--END--" + if occursin("State", l) + # set current state + cur_state = parse(Int64, match(r"\d+", l).match) + 1 + # check if it is accepting + acc = match(r"\{(.*?)\}", l) + if acc != nothing + acc_idx = parse(Int64, acc.match[2:end-1]) + if acc_idx == fin_idx + push!(fin, cur_state) + elseif acc_idx == inf_idx + push!(inf, cur_state) + else + throw("HOAParsingError: failed to assign acceptance condition") + end + end + else + # set edge + input = match(r"\[(.*?)\]", l).match[2:end-1] + inputs = split(input, "&") + for i=1:length(inputs) + inputs[i] = replace(inputs[i], r"\d+" => x->alphabet[parse(Int64, x)+1]) + end + inputs = Set(inputs) + succ = parse(Int64, match(r"\s(.*?)($|\s)", l).match) + 1 + transition[(cur_state, inputs)] = succ + end + l = readline(f) + ln += 1 + end + end + return RabinAutomata{Int64, String}(states, alphabet, transition, initialstate, inf, fin, property) +end + +function parse_alphabet(l::String) + n_inputs = parse(Int64, match(r"\d+", l).match) + alphabet = Vector{String}(undef, n_inputs) + for (i,a) in enumerate(split(l)[3:end]) + # remove quotes + alphabet[i] = a[2:end-1] + end + return alphabet +end + +function automata_type(hoa_file::String) + autom_type = "" + open(hoa_file, "r") do f + l = "" + while autom_type == "" && !eof(f) + l = readline(f) + if occursin("acc-name", l) + if occursin("Rabin", l) + autom_type = "Rabin" + elseif occursin("Buchi", l) + autom_type = "Buchi" + else + throw("HOAParsingError: Automata type not supported, only DFA with Rabin or Buchi acceptance conditions are supported") + end + end + end + end + if autom_type == "" + throw("HOAParsingError: Automata type not found") + end + return autom_type +end \ No newline at end of file diff --git a/test/prototype.jl b/test/prototype.jl index e69a172..61a3c32 100644 --- a/test/prototype.jl +++ b/test/prototype.jl @@ -1,7 +1,115 @@ using Revise using Spot -using LightGraphs -using MetaGraphs + +# using Cxx + +f = ltl"!a U b" + +translator = LTLTranslator(deterministic=true, buchi=true, state_based_acceptance=true) + +aut = translate(translator, f) + +dra = DeterministicRabinAutomata(f) + +f = ltl"(a U b) & GFc & GFd" + +translator = LTLTranslator(deterministic=true, generic=true, state_based_acceptance=true) + +a = translate(LTLTranslator(), f) + +edges(a) + +labs = get_labels(a) + +label_to_array(labs[end]) + +const TRUE_CONSTANT = :true_constant + +function label_to_array(lab::SpotFormula) + @assert is_boolean(lab) + positive_ap = Symbol[] + if length(lab) <= 1 + if @cxx lab.f->is_tt() + push!(positive_ap, TRUE_CONSTANT) + elseif !( @cxx lab.f->is(spot::op::Not) ) + push!(positive_ap, Symbol(lab)) + else + return positive_ap + end + end + cpp_aps = icxx""" + std::vector positive_aps; + for (auto ap: $(f.f)) { + if ( !ap.is(spot::op::Not) ){ + positive_aps.push_back(ap); + } + } + positive_aps; + """ + for ap in cpp_aps + push!(positive_ap, Symbol(SpotFormula(ap))) + end + return positive_ap +end + +function plot(aut) + + +icxx"""$(a.a)->get_dict();""" + + +function get_edges_labels(aut::SpotAutomata) + cpp_edges, cpp_labs = icxx""" + std::vector labs_list; + auto bdict = $(aut.a)->get_dict(); + std::vector> edge_list; + for (auto& e: $(aut.a)->edges()) + { + labs_list.push_back(spot::bdd_to_formula(e.cond, bdict)); + std::vector edge; + edge.push_back(e.src); + edge.push_back(e.dst); + } + """ + return cpp_edges, cpp_labs +end + +cl = get_edges_labels(a) + +cxx"#include " + +edge_it = icxx"""$(a.a)->edges();""" + +cpp_edges = icxx""" + std::vector> edge_list; + for (auto& e: $edge_it) + { + std::vector edge; + edge.push_back(e.src); + edge.push_back(e.dst); + edge_list.push_back(edge); + std::cout << " edge(" << e.src << "-> " << e.dst << ")\n"; + } + edge_list; +""" + +edges = Vector{Tuple{Int64, Int64}}(undef, length(cpp_edges)) +for (i, e) in enumerate(cpp_edges) + edges[i] = (e[0], e[1])) # this is a cpp vector! +end + + + +is_reachability(ltl"F reach") + +atomic_prop_collect(f) + +function isreachability(f::SpotFormula) + icxx""" + spot::formula ff = $(f.f); + ff.is(spot::op::F) && ff[0].is_boolean(); + """ +end ## Get dot string translator = LTLTranslator(state_based_acceptance=true) diff --git a/test/runtests.jl b/test/runtests.jl index a0e046a..2d1cc38 100755 --- a/test/runtests.jl +++ b/test/runtests.jl @@ -1,60 +1,71 @@ -using Spot -using Test -using NBInclude -using TikzPictures - -@testset "LTL Parsing" begin - f = spot.formula("p1 U p2 R (p3 & !p4)") - # convert formula to string - @test f.to_str() == "p1 U (p2 R (p3 & !p4))" - # check properties - @test f.is_ltl_formula() - f = ltl"p1 U p2 R (p3 & !p4)" # check constructor - @test is_ltl_formula(f) - @test is_eventual(ltl"F a") - @test is_sugar_free_ltl(ltl"a & b | c") - @test is_literal(ltl"a") - @test is_literal(ltl"!a") - @test !is_literal(ltl"a & b") - @test is_boolean(ltl"a & b | c") - @test is_reachability(ltl"F reach") - @test is_constrained_reachability(ltl"!avoid U reach") - @test atomic_prop_collect(ltl"a & b & c & d") == [:a,:b,:c,:d] -end - -@testset "LTL To Automata" begin - ltl = ltl"(a U b) & GFc & GFd" - translator = LTLTranslator(deterministic=true, generic=true, state_based_acceptance=true) - a = translate(translator, ltl) -end - -@testset "SpotAutomata" begin - ltl = ltl"(a U b) & GFc & GFd" - a = translate(LTLTranslator(), ltl) - sa = SpotAutomata(a.a) - @test sa == SpotAutomata(a.a, false) - @test num_states(sa) == 2 - @test get_init_state_number(sa) == 1 - @test num_edges(sa) == 6 - @test atomic_propositions(sa) == [:a, :b, :c, :d] -end - -@testset "DRA" begin - dra = DeterministicRabinAutomata(ltl"!a U b") - @test num_states(dra) == 2 - @test get_init_state_number(dra) == 2 - @test nextstate(dra, 2, (:a, :b)) == 1 - @test nextstate(dra, 2, ()) == 2 - @test dra.acc_sets == [(Set([]), Set([1]))] -end - -@testset "doc" begin - @nbinclude(joinpath(@__DIR__, "..", "docs", "spot_basic_tutorial.ipynb")) -end - -@testset "save plot" begin - ltl = ltl"(a U b) & GFc & GFd" - a = translate(LTLTranslator(), ltl) - p = Spot.plot(a) - save(PDF("test"), p) -end \ No newline at end of file +using Spot +using Test +using NBInclude +using TikzPictures + +@testset "LTL Parsing" begin + f = SpotFormula("p1 U p2 R (p3 & !p4)") + # convert formula to string + @test string(f) == "p1 U (p2 R (p3 & !p4))" + # check properties + @test is_ltl_formula(f) + f = ltl"p1 U p2 R (p3 & !p4)" # check constructor + @test is_ltl_formula(f) + @test is_eventual(ltl"F a") + @test is_sugar_free_ltl(ltl"a & b | c") + @test is_literal(ltl"a") + @test is_literal(ltl"!a") + @test !is_literal(ltl"a & b") + @test is_boolean(ltl"a & b | c") + @test is_reachability(ltl"F reach") + @test is_constrained_reachability(ltl"!avoid U reach") + @test atomic_prop_collect(ltl"a & b & c & d") == [:a,:b,:c,:d] +end + +@testset "LTL To Automata" begin + f1 = ltl"(a U b) & GFc & GFd" + translator = LTLTranslator(deterministic=true, generic=true, state_based_acceptance=true) + a = translate(translator, f1) + translator = LTLTranslator(buchi=true) + b = translate(translator, f1) + translator = LTLTranslator(parity=true) + c = translate(translator, f1) +end + +@testset "SpotAutomata" begin + ltl = ltl"(a U b) & GFc & GFd" + a = translate(LTLTranslator(), ltl) + @test num_states(a) == 2 + @test get_init_state_number(a) == 1 + @test num_edges(a) == 6 + @test atomic_propositions(a) == [:a, :b, :c, :d] + sa = split_edges(a) + @test num_states(sa) == num_states(a) + @test num_edges(sa) > num_edges(a) + length(get_edges(a)) == num_edges(a) + length(get_labels(a)) == num_edges(a) + ga = to_generalized_rabin(a) + @test num_states(ga) == num_states(a) # TODO find better test +end + + +@testset "save plot" begin + ltl = ltl"(a U b) & GFc & GFd" + a = translate(LTLTranslator(), ltl) + p = plot_automata(a) + save(PDF("test"), p) +end + +@testset "DRA" begin + dra = DeterministicRabinAutomata(ltl"!a U b") + @test num_states(dra) == 2 + @test get_init_state_number(dra) == 1 + @test nextstate(dra, 1, ()) == 1 + @test nextstate(dra, 1, (:b,)) == 2 + @test nextstate(dra, 2, (:a,:b)) == 2 + @test dra.acc_sets == [(Set([]), Set([2]))] +end + +@testset "doc" begin + @nbinclude(joinpath(@__DIR__, "..", "docs", "spot_basic_tutorial.ipynb")) +end diff --git a/src/spot_cxx.jl b/test/spot_cxx.jl similarity index 67% rename from src/spot_cxx.jl rename to test/spot_cxx.jl index e730027..b4d536d 100644 --- a/src/spot_cxx.jl +++ b/test/spot_cxx.jl @@ -1,129 +1,173 @@ -using Cxx -using Libdl - -const path_to_lib = "/mnt/c/Users/Maxime/wsl/.julia/dev/Spot/deps/spot/lib" -const path_to_header = "/mnt/c/Users/Maxime/wsl/.julia/dev/Spot/deps/spot/include" -addHeaderDir(path_to_header, kind=C_System) -Libdl.dlopen(path_to_lib * "/libspot.so", Libdl.RTLD_GLOBAL) - -cxx"#include " -cxx"#include " -cxx"#include " -cxx"#include " -cxx"#include " -# cxx"#include " - -f = @cxx spot::parse_formula(pointer("FGa")) - -@cxx f -> is_sugar_free_ltl() - -@cxx f -> is_eventual() - -icxx"std::cout << $f << '\n';"; - -# automata conversion - -cxx"spot::translator trans;" - -trans = @cxxnew spot::translator() -autom_type = @cxxnew spot::postprocessor::BA -autom_type = @cxx spot::postprocessor::BA -@cxx trans -> set_type(autom_type) -autom_pref = @cxx spot::postprocessor::Deterministic -@cxx trans -> set_pref(autom_pref) -aut = @cxx trans -> run(f) - -@cxx spot::is_deterministic(aut) - -open("digraph.dot", "w") do io - redirect_stdout(io) do - icxx"print_dot(std::cout, $aut);" - end -end -run(`dot -Tpng digraph.dot -o graph.png`) - -## breaking -open("graph.svg") do f - display("image/svg+xml", read(f, String)) -end - -############################# DRAFT ############################### - -@cxx print_dot(cout, aut) - -cxx""" - std::string graph(const spot::const_twa_ptr & aut){ - std::stringstream buffer; - print_dot(buffer, aut); - return buffer.str(); - } -""" - -s = @cxx graph(aut); - - - -foo = """ - - - -""" - -display("image/svg+xml", foo) - -dg = """ - digraph "" { - rankdir=LR - label="\n[Büchi]" - labelloc="t" - node [shape="circle"] - I [label="", style=invis, width=0] - I -> 0 - 0 [label="0"] - 0 -> 0 [label="1"] - 0 -> 1 [label="a"] - 1 [label="1", peripheries=2] - 1 -> 1 [label="a"] -} -(class std::basic_ostream &) { -} -""" - -run(`dot -Tsvg digraph "" { - rankdir=LR - label="\n[Büchi]" - labelloc="t" - node [shape="circle"] - I [label="", style=invis, width=0] - I -> 0 - 0 [label="0"] - 0 -> 0 [label="1"] - 0 -> 1 [label="a"] - 1 [label="1", peripheries=2] - 1 -> 1 [label="a"] -} -(class std::basic_ostream &) { -} `) - - -function sprint_digraph(io::IO, aut) - (rd, wd) = redirect_stdout(io) do - icxx"std::cout << $aut << '\n';" - end - -end - -digraph = sprint(sprint_digraph, aut) - - -# f2 = @cxx spot::random_ltl() - -io = IOBuffer() -@cxx print_latex_psl(io, f) - -function display_formula(f) - -cxx""" - std::cout << $f << '\n'" - +# Just for prototyping! +using Spot +using Cxx +using Libdl + +const path_to_lib = joinpath(@__DIR__, "deps", "usr", "lib", "libspot.so") +const path_to_header = joinpath(@__DIR__, "deps", "usr", "include") +addHeaderDir(path_to_header, kind=C_System) +Libdl.dlopen(path_to_lib, Libdl.RTLD_GLOBAL) + +struct SpotFormula + f::Cxx.CxxCore.CppValue +end + +cxx"#include " +cxx"#include " +cxx"#include " +cxx"#include " +cxx"#include " +cxx"#include " +cxx"#include " +cxx"#include " +cxx"#include " +cxx"#include " + +f = @cxx spot::parse_formula(pointer("FGa")) +f = SpotFormula(f) + +@cxx f.f -> is_eventual() +is_ltl_formula(f::SpotFormula) = @cxx f.f -> is_ltl_formula() + + +icxx"$f.is(spot::op::G);" + +sap = @cxx spot::atomic_prop_collect(f) + +vap = icxx""" + std::vector v($sap->begin(), $sap->end()); + v; +""" + +function atomic_prop_collect(f) + icxx"std::vector v($sap -> begin(), $sap -> end());" +end + + +sf = icxx"str_psl($f);"; + +String(@cxx spot::str_psl(f)) + +icxx"std::cout << $f << '\n';"; + + +# cxx"#include " + + +@cxx f -> is_sugar_free_ltl() + +@cxx f -> is_eventual() + +icxx"std::cout << $f << '\n';"; + +# automata conversion + + +f = @cxx spot::parse_formula(pointer("(a U b) & GFc & GFd")) + +# cxx"spot::translator trans;" + +trans = @cxx spot::translator() +# autom_type = @cxxnew spot::postprocessor::BA +autom_type = @cxx spot::postprocessor::BA +@cxx trans -> set_type(autom_type) +autom_pref = @cxx spot::postprocessor::Deterministic +@cxx trans -> set_pref(autom_pref) +aut = @cxx trans -> run(f) + +@cxx spot::is_deterministic(aut) + +open("digraph.dot", "w") do io + redirect_stdout(io) do + icxx"print_dot(std::cout, $aut);" + end +end +run(`dot -Tpng digraph.dot -o graph.png`) + +aut = @cxx spot::split_edges(aut) + +## breaking +open("graph.svg") do f + display("image/svg+xml", read(f, String)) +end + +############################# DRAFT ############################### + +@cxx print_dot(cout, aut) + +cxx""" + std::string graph(const spot::const_twa_ptr & aut){ + std::stringstream buffer; + print_dot(buffer, aut); + return buffer.str(); + } +""" + +s = @cxx graph(aut); + + + +foo = """ + + + +""" + +display("image/svg+xml", foo) + +dg = """ + digraph "" { + rankdir=LR + label="\n[Büchi]" + labelloc="t" + node [shape="circle"] + I [label="", style=invis, width=0] + I -> 0 + 0 [label="0"] + 0 -> 0 [label="1"] + 0 -> 1 [label="a"] + 1 [label="1", peripheries=2] + 1 -> 1 [label="a"] +} +(class std::basic_ostream &) { +} +""" + +run(`dot -Tsvg digraph "" { + rankdir=LR + label="\n[Büchi]" + labelloc="t" + node [shape="circle"] + I [label="", style=invis, width=0] + I -> 0 + 0 [label="0"] + 0 -> 0 [label="1"] + 0 -> 1 [label="a"] + 1 [label="1", peripheries=2] + 1 -> 1 [label="a"] +} +(class std::basic_ostream &) { +} `) + + +function sprint_digraph(io::IO, aut) + (rd, wd) = redirect_stdout(io) do + icxx"std::cout << $aut << '\n';" + end + +end + +digraph = sprint(sprint_digraph, aut) + + +# f2 = @cxx spot::random_ltl() + +io = IOBuffer() +@cxx print_latex_psl(io, f) + +function display_formula(f) + +cxx""" + std::cout << $f << '\n'" + cxxt"std::cout" \ No newline at end of file diff --git a/test/test.pdf b/test/test.pdf new file mode 100644 index 0000000..4a395b0 Binary files /dev/null and b/test/test.pdf differ