Merge 4f9246d into 5376efe

Project.toml

@@ -9,9 +9,11 @@ LightGraphs = "093fc24a-ae57-5d10-9952-331d41423f4d"
 MetaGraphs = "626554b9-1ddb-594c-aa3c-2596fe9399a5"
 Parameters = "d96e819e-fc66-5662-9728-84c9c7592b0a"
 PyCall = "438e738f-606a-5dbb-bf0a-cddfbfd45ab0"
+TikzPictures = "37f6aa50-8035-52d0-81c2-5a1d08754b2d"
 
 [extras]
+NBInclude = "0db19996-df87-5ea3-a455-e3a50d440464"
 Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40"
 
 [targets]
-test = ["Test"]
+test = ["NBInclude", "Test"]

src/Spot.jl

@@ -5,6 +5,7 @@ using PyCall
 using Parameters
 using LightGraphs
 using MetaGraphs
+using TikzPictures
 
 const spot = PyNULL()
 
@@ -35,12 +36,6 @@ export
 
 include("formulas.jl")
 
-export
-    LTLTranslator,
-    translate
-
-include("translator.jl")
-
 export
     AbstractAutomata,
     SpotAutomata,
@@ -53,11 +48,20 @@ export
     label_to_array,
     get_rabin_acceptance,
     to_generalized_rabin,
-    is_deterministic,
+    is_deterministic
+
+include("automata.jl")
+
+export
+    LTLTranslator,
+    translate
+
+include("translator.jl")
+
+export
     DeterministicRabinAutomata,
     nextstate
 
-include("automata.jl")
 include("rabin_automata.jl")
 
 end # module spot

src/automata.jl

@@ -140,3 +140,35 @@ function get_inf_fin_sets(aut::SpotAutomata)
     end    
     return (inf_set, fin_set)
 end
+
+## Rendering
+
+function plot(aut::SpotAutomata)
+    autdot = aut.a.to_str(format="dot");
+    texstr = mktempdir() do path
+        dotfile = joinpath(path, "graph.dot")
+        open(dotfile, "w") do f
+            write(f, autdot)
+        end
+        xdotfile = joinpath(path, "graph.xdot")
+        run(pipeline(`dot -Txdot $dotfile `, stdout=xdotfile))
+        texfile = joinpath(path, "graph.tex")
+        run(`dot2tex -tmath --figonly $xdotfile -o $texfile`)
+
+        # a bit hacky, replace the logical characters by latex command
+        texstr = open(texfile) do f
+            texstr = read(f, String)
+            texstr = replace(texstr, "&" => " \\land ")
+            texstr = replace(texstr, "!" => " \\lnot ")
+            texstr = replace(texstr, "|" => "\\lor")
+    #         texstr = replace(texstr, "\$[Büchi]\$" => "[B\\\"uchi]")
+        end
+
+        return texstr
+    end
+    return TikzPicture(texstr, preamble="\n\\usepackage{amsmath,amsfonts,amssymb}\n\\usetikzlibrary{snakes,arrows,shapes}")
+end
+
+function Base.show(f::IO, a::MIME"image/svg+xml", aut::SpotAutomata)
+ 	show(f, a, plot(aut))
+end

src/formulas.jl

@@ -64,3 +64,5 @@ end
 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)]
+
+Base.show(io::IO, m::MIME{Symbol("text/latex")}, f::SpotFormula) = show(io, m, f.f)

src/rabin_automata.jl

@@ -18,7 +18,7 @@ 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), true) # split edges
+    dra = SpotAutomata(translate(translator, ltl).a, true) # split edges
     # dra = to_generalized_rabin(aut) # unclear if needed
     @assert is_deterministic(dra)
     states = 1:num_states(dra)

src/translator.jl

@@ -40,5 +40,5 @@ function translate(translator::LTLTranslator, ltl::SpotFormula, args...)
     translator.generic ? push!(options, "generic") : nothing 
     translator.parity ? push!(options, "parity") : nothing 
     translator.state_based_acceptance ? push!(options, "sbacc") : nothing 
-    return spot.translate(ltl.f, options..., args...)
+    return SpotAutomata(spot.translate(ltl.f, options..., args...))
 end

test/prototype.jl

@@ -3,6 +3,28 @@ using Spot
 using LightGraphs
 using MetaGraphs
 
+## Get dot string 
+translator = LTLTranslator(state_based_acceptance=true)
+aut = translate(translator, ltl"! c U a & !c U b");
+
+autdot = aut.to_str(format="dot");
+
+
+texstr = mktempdir() do path
+    dotfile = joinpath(path, "graph.dot")
+    open(dotfile, "w") do f
+        write(f, autdot)
+    end
+    xdotfile = joinpath(path, "graph.xdot")
+    run(pipeline(`dot -Txdot $dotfile`, stdout=xdotfile))
+    texstr = read(run(`dot2tex $xdotfile`), String)
+end
+
+using TikzPictures
+
+run(`dot -Txdot test.dot | dot2tex > test.tex`)
+
+
 surveillance = ltl"G (F (a & (F (b & Fc))))" 
 safety = ltl"!a U b"
 

test/runtests.jl

@@ -1,5 +1,6 @@
 using Spot
 using Test
+using NBInclude
 
 @testset "LTL Parsing" begin
     f = spot.formula("p1 U p2 R (p3 & !p4)")
@@ -29,8 +30,8 @@ end
 @testset "SpotAutomata" begin
     ltl = ltl"(a U b) & GFc & GFd"
     a = translate(LTLTranslator(), ltl)
-    sa = SpotAutomata(a)
-    @test sa == SpotAutomata(a, false)
+    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
@@ -44,4 +45,8 @@ end
     @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