Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Spot
Spot
Commits
a0a035e0
Commit
a0a035e0
authored
Jan 31, 2015
by
Alexandre Duret-Lutz
Browse files
tgbatest: remove the unused powerset source
* src/tgbatest/powerset.cc: Delete. * src/tgbatest/Makefile.am: Adjust.
parent
7b5f80d4
Changes
2
Hide whitespace changes
Inline
Side-by-side
src/tgbatest/Makefile.am
View file @
a0a035e0
...
...
@@ -37,12 +37,10 @@ check_PROGRAMS = \
checkpsl
\
checkta
\
emptchk
\
expldot
\
intvcomp
\
intvcmp2
\
ltlprod
\
maskacc
\
powerset
\
readsat
\
taatgba
...
...
@@ -53,14 +51,11 @@ checkpsl_SOURCES = checkpsl.cc
checkta_SOURCES
=
checkta.cc
complement_SOURCES
=
complementation.cc
emptchk_SOURCES
=
emptchk.cc
expldot_SOURCES
=
powerset.cc
expldot_CXXFLAGS
=
-DDOTTY
intvcomp_SOURCES
=
intvcomp.cc
intvcmp2_SOURCES
=
intvcmp2.cc
ltl2tgba_SOURCES
=
ltl2tgba.cc
ltlprod_SOURCES
=
ltlprod.cc
maskacc_SOURCES
=
maskacc.cc
powerset_SOURCES
=
powerset.cc
randtgba_SOURCES
=
randtgba.cc
readsat_SOURCES
=
readsat.cc
taatgba_SOURCES
=
taatgba.cc
...
...
src/tgbatest/powerset.cc
deleted
100644 → 0
View file @
7b5f80d4
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2014 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#include
<iostream>
#include
<cassert>
#include
<cstdlib>
#include
"tgbaalgos/powerset.hh"
#include
"tgbaparse/public.hh"
#include
"tgbaalgos/save.hh"
#include
"ltlast/allnodes.hh"
#include
"tgbaalgos/dotty.hh"
void
syntax
(
char
*
prog
)
{
std
::
cerr
<<
prog
<<
" file"
<<
std
::
endl
;
exit
(
2
);
}
int
main
(
int
argc
,
char
**
argv
)
{
int
exit_code
=
0
;
if
(
argc
!=
2
)
syntax
(
argv
[
0
]);
{
auto
dict
=
spot
::
make_bdd_dict
();
spot
::
ltl
::
environment
&
env
(
spot
::
ltl
::
default_environment
::
instance
());
spot
::
tgba_parse_error_list
pel
;
auto
a
=
spot
::
tgba_parse
(
argv
[
1
],
pel
,
dict
,
env
);
if
(
spot
::
format_tgba_parse_errors
(
std
::
cerr
,
argv
[
1
],
pel
))
return
2
;
#ifndef DOTTY
auto
e
=
spot
::
tgba_powerset
(
a
);
spot
::
tgba_save_reachable
(
std
::
cout
,
e
);
#else
spot
::
dotty_reachable
(
std
::
cout
,
a
);
#endif
}
assert
(
spot
::
ltl
::
unop
::
instance_count
()
==
0
);
assert
(
spot
::
ltl
::
binop
::
instance_count
()
==
0
);
assert
(
spot
::
ltl
::
multop
::
instance_count
()
==
0
);
assert
(
spot
::
ltl
::
atomic_prop
::
instance_count
()
!=
0
);
assert
(
spot
::
ltl
::
atomic_prop
::
instance_count
()
==
0
);
return
exit_code
;
}
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment