Commit 3ef91442 authored by Etienne Renault's avatar Etienne Renault

WIP

parent 72d2cf92
Pipeline #19113 failed with stage
in 16 minutes and 36 seconds
......@@ -165,8 +165,8 @@ namespace spot
cspins_iterator::~cspins_iterator()
{
delete[] cond_;
for (auto& s : successors_)
delete[] s;
// for (auto& s : successors_)
// delete[] s;
successors_.clear();
}
......@@ -253,6 +253,7 @@ namespace spot
cspins_state kripkecube<cspins_state, cspins_iterator>::initial(unsigned tid)
{
d_->get_initial_state(inner_[tid].uncompressed);
std::cout << "tid" << tid << std::endl;
return manager_[tid].alloc_setup(inner_[tid].uncompressed,
inner_[tid].compressed,
manager_[tid].size() * 2);
......
......@@ -156,36 +156,47 @@ namespace spot
{
setup();
deadlock_state initial{sys_.initial(tid_)};
if (SPOT_LIKELY(push(initial)))
{
todo_.push_back({initial, sys_.succ(initial.st, tid_), transitions_});
}
while (!todo_.empty() && !stop_.load(std::memory_order_relaxed))
{
if (todo_.back().it->done())
{
pop();
if (deadlock_)
break;
}
else
auto it = sys_.succ(initial.st, tid_);
while (!it->done())
{
++transitions_;
State dst = todo_.back().it->state();
deadlock_state next{dst};
if (SPOT_LIKELY(push(next)))
{
todo_.back().it->next();
todo_.push_back({next, sys_.succ(dst, tid_), transitions_});
}
else
{
todo_.back().it->next();
}
std::cout << "LA\n";
delete it->state();
it-> next();
}
}
delete it;
delete[] initial.st; // FIXME sys.dealloc(sys.st)
finalize();
// if (SPOT_LIKELY(push(initial)))
// {
// todo_.push_back({initial, sys_.succ(initial.st, tid_), transitions_});
// }
// while (!todo_.empty() && !stop_.load(std::memory_order_relaxed))
// {
// if (todo_.back().it->done())
// {
// pop();
// if (deadlock_)
// break;
// }
// else
// {
// ++transitions_;
// State dst = todo_.back().it->state();
// deadlock_state next{dst};
// if (SPOT_LIKELY(push(next)))
// {
// todo_.back().it->next();
// todo_.push_back({next, sys_.succ(dst, tid_), transitions_});
// }
// else
// {
// todo_.back().it->next();
// }
// }
// }
}
bool has_deadlock()
......
......@@ -23,62 +23,62 @@
divine compile > output 2>&1
set -e
if ! test -x "`command -v spins`"; then
echo "spins not installed."
else
# Promela
for opt in '' '--compress 1'; do
run 0 ../modelcheck --is-empty $opt --model $srcdir/elevator2.1.pm \
--formula '!G("req[1]==1" -> (F("p==1" && "cabin_0._pc==2")))'
run 1 ../modelcheck --is-empty $opt --model $srcdir/elevator2.1.pm \
--formula 'F("p==2")'
done
fi
if grep -i -- --ltsmin output; then
:
else
echo "divine not installed, or no ltsmin interface"
exit 77
fi
# dve2
for opt in '' '--compress 1'; do
# The three examples from the README.
# (Don't run the first one using "run 0" because it would take too much
# time with valgrind.).
../modelcheck --is-empty $opt --model $srcdir/beem-peterson.4.dve \
--formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' \
| grep -v pages > stdout1
# same formula, different syntax.
../modelcheck --is-empty $opt --model $srcdir/beem-peterson.4.dve \
--formula '!GF("P_0==CS"|"P_1 == CS"|"P_2 ==CS"|"P_3== CS")' \
| grep -v pages > stdout2
cmp stdout1 stdout2
run 1 ../modelcheck --is-empty $opt --model $srcdir/beem-peterson.4.dve \
--formula '!G(P_0.wait -> F P_0.CS)'
run 1 ../modelcheck --is-empty $opt --model $srcdir/beem-peterson.4.dve\
--formula '!G("pos[1] < 3")'
done
# Now check some error messages.
run 2 ../modelcheck --model foo.dve --formula "F(P_0.CS)" 2>stderr
cat stderr
grep 'Cannot open' stderr
# the dve2C file was generated in the current directory
run 2 ../modelcheck --model beem-peterson.4.dve2C \
--formula 'Xfoo | P_0.f & X"P_0.k < 2xx" | G"pos[0]"' 2>stderr
cat stderr
grep 'No variable' stderr
grep 'No state' stderr
grep 'Unexpected' stderr
# Test parallel algorithms
# set -e
# if ! test -x "`command -v spins`"; then
# echo "spins not installed."
# else
# # Promela
# for opt in '' '--compress 1'; do
# run 0 ../modelcheck --is-empty $opt --model $srcdir/elevator2.1.pm \
# --formula '!G("req[1]==1" -> (F("p==1" && "cabin_0._pc==2")))'
# run 1 ../modelcheck --is-empty $opt --model $srcdir/elevator2.1.pm \
# --formula 'F("p==2")'
# done
# fi
# if grep -i -- --ltsmin output; then
# :
# else
# echo "divine not installed, or no ltsmin interface"
# exit 77
# fi
# # dve2
# for opt in '' '--compress 1'; do
# # The three examples from the README.
# # (Don't run the first one using "run 0" because it would take too much
# # time with valgrind.).
# ../modelcheck --is-empty $opt --model $srcdir/beem-peterson.4.dve \
# --formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' \
# | grep -v pages > stdout1
# # same formula, different syntax.
# ../modelcheck --is-empty $opt --model $srcdir/beem-peterson.4.dve \
# --formula '!GF("P_0==CS"|"P_1 == CS"|"P_2 ==CS"|"P_3== CS")' \
# | grep -v pages > stdout2
# cmp stdout1 stdout2
# run 1 ../modelcheck --is-empty $opt --model $srcdir/beem-peterson.4.dve \
# --formula '!G(P_0.wait -> F P_0.CS)'
# run 1 ../modelcheck --is-empty $opt --model $srcdir/beem-peterson.4.dve\
# --formula '!G("pos[1] < 3")'
# done
# # Now check some error messages.
# run 2 ../modelcheck --model foo.dve --formula "F(P_0.CS)" 2>stderr
# cat stderr
# grep 'Cannot open' stderr
# # the dve2C file was generated in the current directory
# run 2 ../modelcheck --model beem-peterson.4.dve2C \
# --formula 'Xfoo | P_0.f & X"P_0.k < 2xx" | G"pos[0]"' 2>stderr
# cat stderr
# grep 'No variable' stderr
# grep 'No state' stderr
# grep 'Unexpected' stderr
# # Test parallel algorithms
# Test Deadlock
run 0 ../modelcheck --model beem-peterson.4.dve2C \
......@@ -86,14 +86,14 @@ run 0 ../modelcheck --model beem-peterson.4.dve2C \
test `grep "#" stdout | awk -F',' '{print $4}'` = "NO-DEADLOCK"
# Test Bloemen
run 0 ../modelcheck --model beem-peterson.4.dve2C \
--csv --bloemen -p 3 >stdout
test `grep "#" stdout | awk -F',' '{print $7}'` -eq 29115
# # Test Bloemen
# run 0 ../modelcheck --model beem-peterson.4.dve2C \
# --csv --bloemen -p 3 >stdout
# test `grep "#" stdout | awk -F',' '{print $7}'` -eq 29115
run 0 ../modelcheck --model beem-peterson.4.dve2C \
--formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' --csv --bloemen-ec -p 3 >stdout
# run 0 ../modelcheck --model beem-peterson.4.dve2C \
# --formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' --csv --bloemen-ec -p 3 >stdout
# Test CNDFS
run 0 ../modelcheck --model beem-peterson.4.dve2C \
--formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' --csv --cndfs -p 3 >stdout
# # Test CNDFS
# run 0 ../modelcheck --model beem-peterson.4.dve2C \
# --formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' --csv --cndfs -p 3 >stdout
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment