Commit e0cc2673 authored by Hans-Peter Deifel's avatar Hans-Peter Deifel 🐢

Add ZIGZAG example from Högberg et.al.

parent 0d400313
# An automaton that recognizes the tree series ZIGZAG, which is defined as
# follows:
#
# The alphabet Σ = {a/0, s/2} and ZIGZAG maps trees over Σ to ℕ:
#
# ZIGZAG(a) = 1
# ZIGZAG(s(a, _)) = 2
# ZIGZAG(s(s(_, t), _)) = 2 + ZIGZAG(t)
#
# Source: [1, Example 17]
#
# FIXME: R should really be Z, but there is at the time of writing a parser bug
# in Z^X. (See https://git8.cs.fau.de/software/copar/issues/4)
Z × R^({a} + X×X)
l: (1, { inj0 a: 1, inj1 (R, bot): 1, inj1 (r, bot): 1 })
r: (0, { inj0 a: 1, inj1 (bot, L): 1, inj1 (bot, l): 1 })
L: (0, { inj0 a: 1, inj1 (R, bot): 1 })
R: (0, { inj0 a: 1, inj1 (bot, L): 1 })
bot: (0, { inj0 a: 1, inj1 (bot, bot): 1 })
# [1]: Högberg, Johanna, Andreas Maletti, and Jonathan May. “Bisimulation
# Minimisation for Weighted Tree Automata.” In Developments in Language Theory,
# Berlin, Heidelberg: Springer Berlin Heidelberg, 2007.
# https://doi.org/10.1007/978-3-540-73208-2_23.
Block 0: R, bot, L
Block 1: r
Block 2: l
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment