Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Spot
divine-ltsmin-deb
Commits
5fb9135b
Commit
5fb9135b
authored
Sep 04, 2017
by
Alexandre Duret-Lutz
Browse files
Fix some errors reported by g++
parent
aa87eed2
Changes
3
Hide whitespace changes
Inline
Side-by-side
divine/algorithm/map.h
View file @
5fb9135b
...
...
@@ -229,14 +229,14 @@ struct Map : Algorithm, DomainWorker< Map< G, _Statistics > >
if
(
isAccepting
(
t
)
)
extension
(
t
).
map
=
std
::
max
(
extension
(
t
).
map
,
makeId
(
t
)
);
VertexId
map
=
std
::
max
(
extension
(
f
).
map
,
extension
(
t
).
map
);
VertexId
map
_
=
std
::
max
(
extension
(
f
).
map
,
extension
(
t
).
map
);
if
(
extension
(
t
).
map
<
map
)
{
if
(
(
extension
(
t
).
map
)
<
map
_
)
{
// we are *not* the MAP of our successors anymore, so not a
// candidate for elimination (shrinking), remove from set
if
(
isAccepting
(
t
)
&&
extension
(
t
).
elim
)
extension
(
t
).
elim
=
1
;
extension
(
t
).
map
=
map
;
extension
(
t
).
map
=
map
_
;
return
visitor
::
ExpandTransition
;
}
...
...
divine/ltl2ba/ltl.cc
View file @
5fb9135b
...
...
@@ -22,17 +22,17 @@ using namespace divine;
#endif //DOXYGEN_PROCESSING
LTL_parse_t
::
LTL_parse_t
()
:
formule
(
""
)
{
}
{
}
LTL_parse_t
::
LTL_parse_t
(
const
LTL_parse_t
&
a
)
:
formule
(
a
.
formule
)
{
}
LTL_parse_t
::
LTL_parse_t
(
string
&
s
)
:
formule
(
s
)
{
}
LTL_parse_t
::~
LTL_parse_t
()
{
}
void
LTL_parse_t
::
nacti
(
string
&
s
)
{
formule
=
s
;
...
...
@@ -40,14 +40,14 @@ void LTL_parse_t::nacti(string& s)
void
LTL_parse_t
::
nacti
(
void
)
{
#if BUCHI_LANG == BUCHI_LANG_CZ
#if BUCHI_LANG == BUCHI_LANG_CZ
cout
<<
"Zadej LTL formuli> "
;
#elif BUCHI_LANG == BUCHI_LANG_EN
cout
<<
"Enter LTL formula> "
;
#endif
getline
(
cin
,
formule
);
}
void
LTL_parse_t
::
vypis
(
void
)
{
cout
<<
formule
<<
endl
;
...
...
@@ -59,7 +59,7 @@ istream& operator>>(istream& vstup, LTL_parse_t& a)
getline
(
vstup
,
a
.
formule
);
return
(
vstup
);
}
ostream
&
operator
<<
(
ostream
&
vystup
,
LTL_parse_t
a
)
{
vystup
<<
a
.
formule
;
...
...
@@ -106,15 +106,15 @@ void LTL_parse_t::nacti(istream& fr)
enum
synt_an_el
{
un_op
,
bin_op
,
an_left_par
,
an_right_par
,
an_atom
,
an_end
,
an_unknown
,
S
,
A
,
gnd
};
struct
pol_zasobnik
{
int
stav
;
synt_an_el
elem
;
};
struct
preved_zas
{
LTL_syntax_el_t
elem
;
string
pred
;
string
pred
;
int
what
;
// 0 = element; 1 = predikat;
};
...
...
@@ -129,14 +129,14 @@ LTL_syntax_el_t LTL_parse_t::get_syntax_el(int& i, string& pred)
while
(((
formule
[
i
]
==
' '
)
||
(
formule
[
i
]
==
'\t'
)
||
(
formule
[
i
]
==
'\n'
))
&&
(
i
<
delka
))
i
++
;
if
(
i
>=
delka
)
return
(
end
);
if
(
i
>=
delka
)
return
(
ltl_
end
);
switch
(
formule
[
i
])
{
case
'('
:
i
++
;
return
(
left_par
);
break
;
case
')'
:
i
++
;
return
(
right_par
);
break
;
case
'!'
:
i
++
;
return
(
ltl_not
);
break
;
case
'O'
:
case
'X'
:
i
++
;
return
(
ltl_next
);
break
;
case
'X'
:
i
++
;
return
(
ltl_next
);
break
;
case
'U'
:
i
++
;
return
(
ltl_until
);
break
;
case
'W'
:
i
++
;
return
(
ltl_weak
);
break
;
case
'R'
:
...
...
@@ -160,9 +160,9 @@ LTL_syntax_el_t LTL_parse_t::get_syntax_el(int& i, string& pred)
return
(
ltl_ekv
);
}
else
return
(
unknown
);
}
else
return
(
unknown
);
break
;
break
;
case
'F'
:
i
++
;
return
(
ltl_diamond
);
break
;
case
'-'
:
i
++
;
if
(
formule
[
i
]
==
'>'
)
{
case
'-'
:
i
++
;
if
(
formule
[
i
]
==
'>'
)
{
i
++
;
return
(
ltl_impl
);
}
else
return
(
unknown
);
...
...
@@ -213,11 +213,11 @@ synt_an_el konvert_synt_el(LTL_syntax_el_t e)
case
ltl_impl
:
case
ltl_ekv
:
return
(
bin_op
);
break
;
case
right_par
:
return
(
an_right_par
);
break
;
case
left_par
:
return
(
an_left_par
);
break
;
case
left_par
:
return
(
an_left_par
);
break
;
case
ltl_true
:
case
ltl_false
:
case
ltl_atom
:
return
(
an_atom
);
break
;
case
end
:
return
(
an_end
);
break
;
case
ltl_
end
:
return
(
an_end
);
break
;
case
unknown
:
return
(
an_unknown
);
break
;
default:
gerr
<<
"Unexpected value of
\"
e
\"
"
<<
thr
();
return
an_unknown
;
//unreachable
...
...
@@ -250,7 +250,7 @@ bool redukuj(stack<pol_zasobnik>& Z, int pravidlo, synt_an_el& N)
Z
.
pop
();
pom
=
Z
.
top
();
if
(
pom
.
elem
==
bin_op
)
{
Z
.
pop
();
pom
=
Z
.
top
();
if
(
pom
.
elem
==
S
)
{
if
(
pom
.
elem
==
S
)
{
Z
.
pop
();
N
=
S
;
return
(
true
);
}
else
return
(
false
);
...
...
@@ -260,7 +260,7 @@ bool redukuj(stack<pol_zasobnik>& Z, int pravidlo, synt_an_el& N)
case
3
:
pom
=
Z
.
top
();
// S -> (S)
if
(
pom
.
elem
==
an_right_par
)
{
Z
.
pop
();
pom
=
Z
.
top
();
if
(
pom
.
elem
==
S
)
{
if
(
pom
.
elem
==
S
)
{
Z
.
pop
();
pom
=
Z
.
top
();
if
(
pom
.
elem
==
an_left_par
)
{
Z
.
pop
();
...
...
@@ -287,7 +287,7 @@ bool redukuj(stack<pol_zasobnik>& Z, int pravidlo, synt_an_el& N)
case
6
:
pom
=
Z
.
top
();
// A -> (S)
if
(
pom
.
elem
==
an_right_par
)
{
Z
.
pop
();
pom
=
Z
.
top
();
if
(
pom
.
elem
==
S
)
{
if
(
pom
.
elem
==
S
)
{
Z
.
pop
();
pom
=
Z
.
top
();
if
(
pom
.
elem
==
an_left_par
)
{
Z
.
pop
();
...
...
@@ -424,7 +424,7 @@ bool LTL_parse_t::syntax_check(LTL_formul_t& F)
if
((
N
==
gnd
)
&&
(
an_elem
==
un_op
))
{
pom
.
elem
=
an_elem
;
pom
.
stav
=
2
;
Z
.
push
(
pom
);
stav
=
2
;
stav
=
2
;
prev_pom
.
what
=
0
;
prev_pom
.
elem
=
elem
;
...
...
@@ -495,7 +495,7 @@ bool LTL_parse_t::syntax_check(LTL_formul_t& F)
break
;
}
if
((
N
==
gnd
)
&&
(
an_elem
==
an_left_par
))
{
pom
.
stav
=
8
;
pom
.
elem
=
an_elem
;
pom
.
stav
=
8
;
pom
.
elem
=
an_elem
;
Z
.
push
(
pom
);
stav
=
8
;
break
;
}
...
...
@@ -588,14 +588,14 @@ bool LTL_parse_t::syntax_check(LTL_formul_t& F)
F1
.
clear
();
F2
.
clear
();
F1
=
ZF
.
top
();
ZF
.
pop
();
prev_pom
=
Zprev
.
top
();
prev_pom
=
Zprev
.
top
();
Zprev
.
pop
();
preved_un_op
(
prev_pom
.
elem
,
F1
,
F2
);
ZF
.
push
(
F2
);
}
else
stav
=
-
1
;
}
else
stav
=
-
1
;
break
;
}
stav
=
-
1
;
break
;
stav
=
-
1
;
break
;
case
7
:
if
(
N
==
A
)
{
pom
.
stav
=
12
;
pom
.
elem
=
A
;
Z
.
push
(
pom
);
...
...
@@ -637,7 +637,7 @@ bool LTL_parse_t::syntax_check(LTL_formul_t& F)
if
((
N
==
gnd
)
&&
(
an_elem
==
un_op
))
{
pom
.
elem
=
an_elem
;
pom
.
stav
=
2
;
Z
.
push
(
pom
);
stav
=
2
;
stav
=
2
;
prev_pom
.
what
=
0
;
prev_pom
.
elem
=
elem
;
...
...
@@ -647,7 +647,7 @@ bool LTL_parse_t::syntax_check(LTL_formul_t& F)
if
((
N
==
gnd
)
&&
(
an_elem
==
an_atom
))
{
pom
.
elem
=
an_elem
;
pom
.
stav
=
4
;
Z
.
push
(
pom
);
stav
=
4
;
stav
=
4
;
prev_pom
.
what
=
1
;
prev_pom
.
pred
=
pred
;
...
...
@@ -737,7 +737,7 @@ bool LTL_parse_t::syntax_check(LTL_formul_t& F)
prev_pom
.
elem
=
elem
;
Zprev
.
push
(
prev_pom
);
break
;
}
}
if
((
N
==
gnd
)
&&
(
an_elem
==
an_right_par
))
{
pom
.
elem
=
an_elem
;
pom
.
stav
=
15
;
Z
.
push
(
pom
);
...
...
divine/ltl2ba/ltl.hh
View file @
5fb9135b
...
...
@@ -20,7 +20,7 @@ namespace divine {
enum
LTL_syntax_el_t
{
ltl_box
,
ltl_diamond
,
ltl_not
,
ltl_next
,
ltl_until
,
ltl_V
,
ltl_and
,
ltl_or
,
ltl_xor
,
ltl_impl
,
ltl_ekv
,
ltl_weak
,
ltl_true
,
ltl_false
,
ltl_atom
,
left_par
,
right_par
,
unknown
,
end
};
ltl_true
,
ltl_false
,
ltl_atom
,
left_par
,
right_par
,
unknown
,
ltl_
end
};
/* Syntactic elements - unary operators, binary operators, true,
false, atom, parenthesis, unknown element, end of formula
*/
...
...
@@ -30,7 +30,7 @@ enum LTL_syntax_el_t {ltl_box, ltl_diamond, ltl_not, ltl_next, ltl_until,
class
LTL_parse_t
{
private:
string
formule
;
/* helping method */
LTL_syntax_el_t
get_syntax_el
(
int
&
i
,
string
&
pred
);
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a 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