package fadecider

  1. Overview
  2. Docs
A package for deciding universality and subsumption of omega automata using Ramsey-based methods

Install 

dune-project
 Dependency

github.com Readme Changelog BSD-3-clause License Edit opam file Versions (1)

Authors

  1. O
    Oliver Friedmann
  2. F
    Felix Klaedtke
  3. M
    Martin Lange

Maintainers

  1. O
    Oliver Friedmann
  2. F
    Felix Klaedtke
  3. M
    Martin Lange

Sources

fadecider-0.7.tbz
sha256=7a27293d686ddd068a7247693ca8f48b524041ae6b6e9e40438571213bc3728b
sha512=020e418ec241463287b9d56c2a1b840a5f2f68892b703fe17427669be32225c8760751f588e5991cbffc96e9cd09204d4ecb77dfdcb0f6216b200419ded5a6ae

doc/fadecider/Taggedtrapo/TaggedStatesetSet/index.html

Module Taggedtrapo.TaggedStatesetSetSource

Sourcetype ('q, 'a, 'p) t
Sourceval empty : ('q, 'a, _, _, 'p, _, _) MetaTaggedTrapo.t -> ('q, 'a, 'p) t
Sourceval epsilon : ('q, 'a, _, _, 'p, _, _) MetaTaggedTrapo.t -> ('q, 'a, 'p) t
Sourceval subsumed : ('q, 'a, 'p) t -> 'p -> 'q Tcsset.TreeSet.t -> bool
Sourceval add : ('q, 'a, _, _, 'p, _, _) MetaTaggedTrapo.t -> ('q, 'a, 'p) t -> 'p -> 'q Tcsset.TreeSet.t -> 'a Tcsautomata.Alphabet.word -> ('q, 'a, 'p) t
Sourceval union : ('q, 'a, 'p) t -> ('q, 'a, 'p) t -> ('q, 'a, 'p) t
Sourceval reacher_idempot_match : ('q, 'a, _, _, 'p, _, _) MetaTaggedTrapo.t -> ('q, 'a, 'p) t -> ('q, 'a, 'p) t -> string option