Spot January 2021

spot@lrde.epita.fr

2 participants
2 discussions

Walking through BDD formula in python
by Ayrat Khalimov 26 May '21

26 May '21

hi! With the aid of SPOT I am developing a counter-example guided synthesizer in python. See [1] if interested for details. My question is: I am trying to parse twa_run in python, namely, parse the labels of the each step (`spot.impl.step`). Is there a python way to walk through BDD? (The label is a simple cube expressed in BDD, and I need to convert it into my internal structure) (yes, this is rather a question about python interface for buddy) (no, that is not feature request:) if not possible, I will simply print the label and parse the string, that is not crucial) [1] The idea is - guess the model, - then model check it and get a counter-example - then encode the counter-example into the "guesser" (which uses an SMT solver) thanks, Ayrat

2 5

LTLf simplification
by Walke, Homer 04 Jan '21

04 Jan '21

Hi! I know Spot doesn't provide much support for LTLf (LTL with finite trace semantics) but I need to simplify some LTLf formulas. I was wondering which tl_simplifier_options, if any, would simplify according to the semantics of LTLf, i.e reduce_basics, synt_impl, etc. I know that using all the rewritings wouldn't work since many of them only apply to LTL and not LTLf but I'd like to use any rewritings that do apply to LTLf. Would anyone be able to point me in the right direction? Alternatively do you know of another software package that might do LTLf simplification? Thanks! Homer

2 1

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Spot January 2021