alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* spot/twaalgos/dualize.cc: Improve comment.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2019-07-30 15:34:02 +02:00
parent 8ec6ea838d
commit 95087030b0
1 changed files with 7 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

13
spot/twaalgos/dualize.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement // Copyright (C) 2017-2019 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -181,11 +181,12 @@ namespace spot
} }
// Handles the dualization of a universal initial transition. // Handles the dualization of a universal initial transition.
// In theory the transition would be split into several existential // In theory the transition would be split into several
// initial transitions, but since spot does not allow multiple initial // existential initial transitions, but since Spot does not
// states, we rather use a trick: We add a new initial state, and then // allow multiple initial states, we rather use a trick: We add
// copy all exiting transitions from each of the state of the universal // a new initial state, and then copy all exiting transitions
// initial transition. // from each destination states of the universal initial
// transition.
void univ_init(const twa_graph_ptr& res) void univ_init(const twa_graph_ptr& res)
{ {
bdd comb = bddfalse; bdd comb = bddfalse;