Spot October 2011

spot@lrde.epita.fr

2 participants
2 discussions

spot-beginner questions
by Nikos Gorogiannis 17 Nov '11

17 Nov '11

Hi, I'm trying to learn spot, and I want to run an emptiness check on a product of two automata which I will be creating by subclassing tgba. The two automata have overlapping, but different, signatures i.e. atomic propositions. If I understand correctly, I cannot achieve this by using two different bdd_dicts, as the two automata passed to the product object must share the same bdd_dict. How does one deal with this problem in spot? Thanks Nikos

2 13

self-modifying automaton
by Nikos Gorogiannis 07 Oct '11

07 Oct '11

Hi, I've been looking for a library that would allow me to provide a (lazy) interface for enumerating the states of an automaton and doing on-the-fly model checking. Spot looks like exactly what I need! (which is great; I couldn't find any other tool supporting custom model checking like this). What I will need on top of this, is when the emptiness check fails, I'd like to modify the automaton using the information provided by the check and re-run the check. Changes to the automaton will be localized, so destroying and rebuilding the objects relating to the emptiness check seems unnecessarily expensive. Is there any way around this? Best regards Nikos Gorogiannis

2 2

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Spot October 2011