Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Reduce: Simulation algorithm #434

Draft
wants to merge 8 commits into
base: devel
Choose a base branch
from
Draft

Reduce: Simulation algorithm #434

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
c3d9118
Reduce: Simulation algorithm
samo538 Aug 4, 2024
aa3ccd6
Reduce: Benchmarking
samo538 Sep 2, 2024
07df042
Fix: benchmarking automata
samo538 Sep 4, 2024
7599acf
1. Update: Matrix removal
samo538 Oct 7, 2024
550c81d
reduced number of binary searches
samo538 Oct 25, 2024
178a790
Deleted hash map
samo538 Nov 26, 2024
d232b58
reduced binary searches
samo538 Nov 26, 2024
1bbd7ea
faster vector, better loops
samo538 Dec 20, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
130 changes: 129 additions & 1 deletion src/nfa/operations.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,10 @@
#include <list>
#include <unordered_set>
#include <iterator>
#include <unordered_map>

// MATA headers
#include "mata/alphabet.hh"
#include "mata/nfa/delta.hh"
#include "mata/utils/sparse-set.hh"
#include "mata/nfa/nfa.hh"
Expand Down Expand Up @@ -39,7 +41,7 @@ namespace {
throw std::runtime_error("all symbols are used, we cannot compute simulation reduction");
}
}

const size_t state_num{ aut.num_of_states() };
Simlib::ExplicitLTS lts_for_simulation(state_num);

Expand All @@ -56,6 +58,129 @@ namespace {
return lts_for_simulation.compute_simulation();
}

int index_fn(int alph, int x, int y, size_t alph_size, size_t no_states){
return alph + x * alph_size + y * alph_size * no_states;
}

Simlib::Util::BinaryRelation compute_iny_direct_simulation(const Nfa& aut) {
// ! Preprocessing
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is the format // ! supposed to mean something specific? Like a critical section or something? I use this notation to highlight something important. Like a note of warning etc. This does not look like this case, however.

Copy link
Author

@samo538 samo538 Aug 28, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The pseudo code for this algorithm is "split" into sections with these descriptions. I tried make clear which parts of the real code represent which parts of the pseudo code.

Copy link
Collaborator

@Adda0 Adda0 Aug 29, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sounds good. Great idea. And it makes reading the code much easier. I would however use a more readable notation. Something like // Pseudocode: Preprocessing. or similar. Otherwise, everyone will be unsure of what the // ! should represent.

Nfa reverted_nfa;
std::vector<std::vector<bool>> result_sim_tmp {}; // R_tmp
std::vector<std::pair<State, State>> worklist {}; // Worklist

// Alphabet extraction
mata::OnTheFlyAlphabet alph;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Since you are extracting the alphabet from the automaton, you could also add the alphabet as an optional parameter (probably const Alphabet* alphabet = nullptr) to the reduction function and fill the alphabet manually here only when the optional parameter is left empty.

aut.fill_alphabet(alph);
std::vector<Symbol> alph_syms = alph.get_alphabet_symbols().to_vector();

size_t no_states = aut.num_of_states();
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

When you define variables which will not change in the future, use const to help the optimizer optimize the code further.

PS: We usually use num_<something>, <something>_num etc. for variable containing a number of something in Mata.

size_t matrix_size = no_states * no_states * alph_syms.size();

std::vector<unsigned> matrix (matrix_size, 0); // Stores the value of cnt()
std::vector<unsigned> index_map {}; // Associates every Symbol with unique value
std::vector<bool> usage_map (alph_syms.size(), false); // Storing usage of Symbols

result_sim_tmp.resize(no_states);
for (size_t i = 0; i < no_states; i++){
result_sim_tmp[i].resize(no_states, true);
}

// This is very memory inefficient
for (size_t x = 0; x < alph_syms.size(); x++){ // Indexing every Symbol with an number
if (index_map.size() <= alph_syms[x]){
index_map.resize(alph_syms[x] + 1 ,0);
}
index_map[alph_syms[x]] = x;
}

reverted_nfa = revert(aut); // Reverted NFA
// ! End of preprocessing

// ! Initial refinement
for (size_t p = 0; p < no_states; p++) {
for (size_t q = 0; q < no_states; q++) {
// Check final
if (aut.final.contains(p) && !aut.final.contains(q)) {
if (result_sim_tmp[p][q] != false) {
worklist.push_back(std::pair(p,q)); // worklist append
result_sim_tmp[p][q] = false;
}
}

auto symbol_q = aut.delta[q].begin();
auto sym_end = aut.delta[q].end();
for (size_t x = 0; x < alph_syms.size(); x++) {
if (symbol_q == sym_end){ // If we searched all symbols
break;
}

size_t q_size;
Symbol active_sym = (*symbol_q).symbol; // Get the active symbol
usage_map[index_map[active_sym]] = true; // Mark the symbol as used

q_size = (*symbol_q).num_of_targets(); // Compute lenght and store it
matrix[index_fn(index_map[active_sym], p, q, alph_syms.size(), no_states)] = q_size;
std::advance(symbol_q, 1);
}

auto active_sym = aut.delta[p].begin();
sym_end = aut.delta[p].end();
for(size_t x = 0; x < alph_syms.size(); x++){
if (active_sym == sym_end){ // If we searched all symbols
break;
}
bool is_present = usage_map[index_map[(*active_sym).symbol]]; // get the index of the symbol
if (is_present == false){
if (result_sim_tmp[p][q] != false) {
worklist.push_back(std::pair(p,q)); // worklist append
result_sim_tmp[p][q] = false;
}
}
std::advance(active_sym, 1);
}

std::fill(usage_map.begin(), usage_map.end(), false);
}
}
// ! End of initial refinement

// ! Propagate until fixpoint
size_t worklist_size;
std::pair<State, State> working_pair;
while ((worklist_size = worklist.size()) != 0) {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

maybe just use worklist.size()? compiler should be able to optimize the two calls...

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Testing for (non-)emptiness should be done using worklist.empty(), optionally with ! in front of the expression for non-emptiness. And we can then use size() inside the loop body.

working_pair = worklist[worklist_size - 1];
worklist.pop_back();

auto symbol_q_ = reverted_nfa.delta[working_pair.second].begin();
auto sym_end = reverted_nfa.delta[working_pair.second].end();
for (size_t x = 0; x < alph_syms.size(); x++) {
if (symbol_q_ == sym_end){ // If we searched all symbols
break;
}
Symbol active_sym = (*symbol_q_).symbol;
for (State q: (*symbol_q_).targets.to_vector()) {
if (--matrix[index_fn(index_map[active_sym], working_pair.first, q, alph_syms.size(), no_states)] == 0) {
auto symbol_p_ = reverted_nfa.delta[working_pair.first].find(active_sym);
if (symbol_p_ == reverted_nfa.delta[working_pair.first].end()) {
continue;
}
for (State p: (*symbol_p_).targets.to_vector()) {
if (result_sim_tmp[p][q] != false) {
worklist.push_back(std::pair(p,q)); // worklist append
result_sim_tmp[p][q] = false;
}
}
}
}
std::advance(symbol_q_, 1);
}
}
// ! End of Propagate until fixpoint

Simlib::Util::BinaryRelation tmp {result_sim_tmp};
return tmp;
}

Nfa reduce_size_by_simulation(const Nfa& aut, StateRenaming &state_renaming) {
Nfa result;
const auto sim_relation = algorithms::compute_relation(
Expand Down Expand Up @@ -993,6 +1118,9 @@ Simlib::Util::BinaryRelation mata::nfa::algorithms::compute_relation(const Nfa&
if ("simulation" == relation && direction == "forward") {
return compute_fw_direct_simulation(aut);
}
else if ("simulation" == relation && direction == "iny") {
return compute_iny_direct_simulation(aut);
}
else {
throw std::runtime_error(std::to_string(__func__) +
" received an unknown value of the \"relation\" key: " + relation);
Expand Down
2 changes: 1 addition & 1 deletion tests-integration/automata/b-armc-incl-easiest/aut1.mata
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
@NFA-bits
%Initial q0
%Final !q0 & !q2 & !q3
%Final !q0 & !q2 & !q3
q0 (!a1 & a2 & a3 & a4 & !a5) q3
q0 (a1 & !a2 & a3 & a4 & !a5) q3
q1 (a1 & a2 & a3 & a4 & a5) q1
Expand Down
2 changes: 1 addition & 1 deletion tests-integration/automata/b-armc-incl-easiest/aut2.mata
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
@NFA-bits
%Initial q0
%Final !q0 & !q2 & !q3 & !q4 & !q5 & !q6 & !q7 & !q8 & !q9 & !q10 & !q11 & !q12 & !q13 & !q14 & !q15 & !q16 & !q17 & !q18 & !q19 & !q20 & !q21 & !q22 & !q23 & !q24 & !q25 & !q26 & !q27 & !q28 & !q29 & !q30 & !q31 & !q32 & !q33 & !q34 & !q35 & !q36 & !q37 & !q38 & !q39 & !q40 & !q41 & !q42 & !q43 & !q44 & !q45 & !q46 & !q47 & !q48 & !q49 & !q50 & !q51 & !q52 & !q53 & !q54 & !q55 & !q56 & !q57 & !q58 & !q59 & !q60 & !q61 & !q62 & !q63 & !q64 & !q65 & !q66 & !q67 & !q68 & !q69 & !q70 & !q71 & !q72 & !q73 & !q74 & !q75 & !q76 & !q77 & !q78 & !q79 & !q80 & !q81 & !q82 & !q83 & !q84 & !q85 & !q86 & !q87 & !q88 & !q89 & !q90 & !q91 & !q92 & !q93 & !q94 & !q95 & !q96 & !q97 & !q98 & !q99 & !q100 & !q101 & !q102 & !q103 & !q104 & !q105 & !q106 & !q107 & !q108 & !q109 & !q110 & !q111 & !q112 & !q113 & !q114 & !q115 & !q116 & !q117 & !q118 & !q119 & !q120 & !q121 & !q122 & !q123 & !q124 & !q125 & !q126 & !q127 & !q128 & !q129 & !q130 & !q131 & !q132 & !q133 & !q134 & !q135 & !q136 & !q137 & !q138 & !q139 & !q140 & !q141 & !q142 & !q143 & !q144 & !q145 & !q146 & !q147 & !q148 & !q149 & !q150 & !q151 & !q152 & !q153 & !q154 & !q155 & !q156 & !q157 & !q158 & !q159 & !q160 & !q161 & !q162 & !q163 & !q164 & !q165 & !q166 & !q167 & !q168 & !q169 & !q170 & !q171 & !q172 & !q173 & !q174 & !q175 & !q176 & !q177 & !q178 & !q179 & !q180 & !q181 & !q182 & !q183 & !q184 & !q185 & !q186 & !q187 & !q188 & !q189 & !q190 & !q191 & !q192 & !q193 & !q194 & !q195 & !q196 & !q197 & !q198 & !q199 & !q200 & !q201 & !q202 & !q203 & !q204 & !q205 & !q206 & !q207 & !q208 & !q209 & !q210 & !q211 & !q212 & !q213 & !q214 & !q215 & !q216 & !q217 & !q218 & !q219 & !q220 & !q221 & !q222 & !q223 & !q224 & !q225 & !q226 & !q227 & !q228 & !q229 & !q230 & !q231 & !q232 & !q233 & !q234 & !q235 & !q236 & !q237 & !q238 & !q239 & !q240 & !q241 & !q242 & !q243 & !q244 & !q245 & !q246 & !q247 & !q248 & !q249 & !q250 & !q251 & !q252 & !q253 & !q254 & !q255
%Final !q0 & !q2 & !q3 & !q4 & !q5 & !q6 & !q7 & !q8 & !q9 & !q10 & !q11 & !q12 & !q13 & !q14 & !q15 & !q16 & !q17 & !q18 & !q19 & !q20 & !q21 & !q22 & !q23 & !q24 & !q25 & !q26 & !q27 & !q28 & !q29 & !q30 & !q31 & !q32 & !q33 & !q34 & !q35 & !q36 & !q37 & !q38 & !q39 & !q40 & !q41 & !q42 & !q43 & !q44 & !q45 & !q46 & !q47 & !q48 & !q49 & !q50 & !q51 & !q52 & !q53 & !q54 & !q55 & !q56 & !q57 & !q58 & !q59 & !q60 & !q61 & !q62 & !q63 & !q64 & !q65 & !q66 & !q67 & !q68 & !q69 & !q70 & !q71 & !q72 & !q73 & !q74 & !q75 & !q76 & !q77 & !q78 & !q79 & !q80 & !q81 & !q82 & !q83 & !q84 & !q85 & !q86 & !q87 & !q88 & !q89 & !q90 & !q91 & !q92 & !q93 & !q94 & !q95 & !q96 & !q97 & !q98 & !q99 & !q100 & !q101 & !q102 & !q103 & !q104 & !q105 & !q106 & !q107 & !q108 & !q109 & !q110 & !q111 & !q112 & !q113 & !q114 & !q115 & !q116 & !q117 & !q118 & !q119 & !q120 & !q121 & !q122 & !q123 & !q124 & !q125 & !q126 & !q127 & !q128 & !q129 & !q130 & !q131 & !q132 & !q133 & !q134 & !q135 & !q136 & !q137 & !q138 & !q139 & !q140 & !q141 & !q142 & !q143 & !q144 & !q145 & !q146 & !q147 & !q148 & !q149 & !q150 & !q151 & !q152 & !q153 & !q154 & !q155 & !q156 & !q157 & !q158 & !q159 & !q160 & !q161 & !q162 & !q163 & !q164 & !q165 & !q166 & !q167 & !q168 & !q169 & !q170 & !q171 & !q172 & !q173 & !q174 & !q175 & !q176 & !q177 & !q178 & !q179 & !q180 & !q181 & !q182 & !q183 & !q184 & !q185 & !q186 & !q187 & !q188 & !q189 & !q190 & !q191 & !q192 & !q193 & !q194 & !q195 & !q196 & !q197 & !q198 & !q199 & !q200 & !q201 & !q202 & !q203 & !q204 & !q205 & !q206 & !q207 & !q208 & !q209 & !q210 & !q211 & !q212 & !q213 & !q214 & !q215 & !q216 & !q217 & !q218 & !q219 & !q220 & !q221 & !q222 & !q223 & !q224 & !q225 & !q226 & !q227 & !q228 & !q229 & !q230 & !q231 & !q232 & !q233 & !q234 & !q235 & !q236 & !q237 & !q238 & !q239 & !q240 & !q241 & !q242 & !q243 & !q244 & !q245 & !q246 & !q247 & !q248 & !q249 & !q250 & !q251 & !q252 & !q253 & !q254 & !q255
q0 (a1 & a2 & a3 & a4 & !a5) q184
q0 (!a1 & a2 & a3 & a4 & !a5) q181
q0 (a1 & !a2 & a3 & a4 & !a5) q185
Expand Down
2 changes: 1 addition & 1 deletion tests-integration/automata/b-armc-incl-easy/aut1.mata
View file
Open in desktop

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion tests-integration/automata/b-armc-incl-easy/aut2.mata
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
@NFA-bits
%Initial q0
%Final !q0 & !q2 & !q3 & !q4 & !q5 & !q6 & !q7 & !q8 & !q9 & !q10 & !q11 & !q12 & !q13 & !q14 & !q15 & !q16 & !q17 & !q18 & !q19 & !q20 & !q21 & !q22 & !q23 & !q24 & !q25 & !q26 & !q27 & !q28 & !q29 & !q30 & !q31 & !q32 & !q33 & !q34 & !q35 & !q36 & !q37 & !q38 & !q39 & !q40 & !q41 & !q42 & !q43 & !q44 & !q45 & !q46 & !q47 & !q48 & !q49 & !q50 & !q51 & !q52 & !q53 & !q54 & !q55 & !q56 & !q57 & !q58 & !q59 & !q60 & !q61 & !q62 & !q63 & !q64 & !q65 & !q66 & !q67 & !q68 & !q69 & !q70 & !q71 & !q72 & !q73 & !q74 & !q75 & !q76 & !q77 & !q78 & !q79 & !q80 & !q81 & !q82 & !q83 & !q84 & !q85 & !q86 & !q87 & !q88 & !q89 & !q90 & !q91 & !q92 & !q93 & !q94 & !q95 & !q96 & !q97 & !q98 & !q99 & !q100 & !q101 & !q102 & !q103 & !q104 & !q105 & !q106 & !q107 & !q108 & !q109 & !q110 & !q111 & !q112 & !q113 & !q114 & !q115 & !q116 & !q117 & !q118 & !q119 & !q120 & !q121 & !q122 & !q123 & !q124 & !q125 & !q126 & !q127 & !q128 & !q129 & !q130 & !q131 & !q132 & !q133 & !q134 & !q135 & !q136 & !q137 & !q138 & !q139 & !q140 & !q141 & !q142 & !q143 & !q144 & !q145 & !q146 & !q147 & !q148 & !q149 & !q150 & !q151 & !q152 & !q153 & !q154 & !q155 & !q156 & !q157 & !q158 & !q159 & !q160 & !q161 & !q162 & !q163 & !q164 & !q165 & !q166 & !q167 & !q168 & !q169 & !q170 & !q171 & !q172 & !q173 & !q174 & !q175 & !q176 & !q177 & !q178 & !q179 & !q180 & !q181 & !q182 & !q183 & !q184 & !q185 & !q186 & !q187 & !q188 & !q189 & !q190 & !q191 & !q192 & !q193 & !q194 & !q195 & !q196 & !q197 & !q198 & !q199 & !q200 & !q201 & !q202 & !q203 & !q204 & !q205 & !q206 & !q207 & !q208 & !q209 & !q210 & !q211 & !q212 & !q213 & !q214 & !q215 & !q216 & !q217 & !q218 & !q219 & !q220 & !q221 & !q222 & !q223 & !q224 & !q225 & !q226 & !q227 & !q228 & !q229 & !q230 & !q231 & !q232 & !q233 & !q234 & !q235 & !q236 & !q237 & !q238 & !q239 & !q240 & !q241 & !q242 & !q243 & !q244 & !q245 & !q246 & !q247 & !q248 & !q249 & !q250 & !q251 & !q252 & !q253 & !q254 & !q255 & !q256 & !q257 & !q258 & !q259 & !q260 & !q261 & !q262 & !q263 & !q264 & !q265 & !q266 & !q267 & !q268 & !q269 & !q270 & !q271 & !q272 & !q273 & !q274 & !q275 & !q276 & !q277 & !q278 & !q279 & !q280 & !q281 & !q282 & !q283 & !q284 & !q285 & !q286 & !q287 & !q288 & !q289 & !q290 & !q291 & !q292 & !q293 & !q294 & !q295 & !q296 & !q297 & !q298 & !q299 & !q300 & !q301 & !q302 & !q303 & !q304 & !q305 & !q306 & !q307 & !q308 & !q309 & !q310 & !q311 & !q312 & !q313 & !q314 & !q315 & !q316 & !q317 & !q318 & !q319 & !q320 & !q321 & !q322 & !q323 & !q324 & !q325 & !q326 & !q327 & !q328 & !q329 & !q330 & !q331 & !q332 & !q333 & !q334 & !q335 & !q336 & !q337 & !q338 & !q339 & !q340 & !q341 & !q342 & !q343 & !q344 & !q345 & !q346 & !q347 & !q348 & !q349 & !q350 & !q351 & !q352 & !q353 & !q354 & !q355 & !q356 & !q357 & !q358 & !q359 & !q360 & !q361 & !q362 & !q363 & !q364 & !q365 & !q366 & !q367 & !q368 & !q369 & !q370 & !q371 & !q372 & !q373 & !q374 & !q375 & !q376 & !q377 & !q378 & !q379 & !q380 & !q381 & !q382 & !q383 & !q384 & !q385 & !q386 & !q387 & !q388 & !q389 & !q390 & !q391 & !q392 & !q393 & !q394 & !q395 & !q396 & !q397 & !q398 & !q399 & !q400 & !q401 & !q402 & !q403 & !q404 & !q405 & !q406 & !q407 & !q408 & !q409 & !q410 & !q411 & !q412 & !q413 & !q414 & !q415 & !q416 & !q417 & !q418 & !q419 & !q420 & !q421 & !q422 & !q423 & !q424 & !q425 & !q426 & !q427 & !q428 & !q429 & !q430 & !q431 & !q432 & !q433
%Final !q0 & !q2 & !q3 & !q4 & !q5 & !q6 & !q7 & !q8 & !q9 & !q10 & !q11 & !q12 & !q13 & !q14 & !q15 & !q16 & !q17 & !q18 & !q19 & !q20 & !q21 & !q22 & !q23 & !q24 & !q25 & !q26 & !q27 & !q28 & !q29 & !q30 & !q31 & !q32 & !q33 & !q34 & !q35 & !q36 & !q37 & !q38 & !q39 & !q40 & !q41 & !q42 & !q43 & !q44 & !q45 & !q46 & !q47 & !q48 & !q49 & !q50 & !q51 & !q52 & !q53 & !q54 & !q55 & !q56 & !q57 & !q58 & !q59 & !q60 & !q61 & !q62 & !q63 & !q64 & !q65 & !q66 & !q67 & !q68 & !q69 & !q70 & !q71 & !q72 & !q73 & !q74 & !q75 & !q76 & !q77 & !q78 & !q79 & !q80 & !q81 & !q82 & !q83 & !q84 & !q85 & !q86 & !q87 & !q88 & !q89 & !q90 & !q91 & !q92 & !q93 & !q94 & !q95 & !q96 & !q97 & !q98 & !q99 & !q100 & !q101 & !q102 & !q103 & !q104 & !q105 & !q106 & !q107 & !q108 & !q109 & !q110 & !q111 & !q112 & !q113 & !q114 & !q115 & !q116 & !q117 & !q118 & !q119 & !q120 & !q121 & !q122 & !q123 & !q124 & !q125 & !q126 & !q127 & !q128 & !q129 & !q130 & !q131 & !q132 & !q133 & !q134 & !q135 & !q136 & !q137 & !q138 & !q139 & !q140 & !q141 & !q142 & !q143 & !q144 & !q145 & !q146 & !q147 & !q148 & !q149 & !q150 & !q151 & !q152 & !q153 & !q154 & !q155 & !q156 & !q157 & !q158 & !q159 & !q160 & !q161 & !q162 & !q163 & !q164 & !q165 & !q166 & !q167 & !q168 & !q169 & !q170 & !q171 & !q172 & !q173 & !q174 & !q175 & !q176 & !q177 & !q178 & !q179 & !q180 & !q181 & !q182 & !q183 & !q184 & !q185 & !q186 & !q187 & !q188 & !q189 & !q190 & !q191 & !q192 & !q193 & !q194 & !q195 & !q196 & !q197 & !q198 & !q199 & !q200 & !q201 & !q202 & !q203 & !q204 & !q205 & !q206 & !q207 & !q208 & !q209 & !q210 & !q211 & !q212 & !q213 & !q214 & !q215 & !q216 & !q217 & !q218 & !q219 & !q220 & !q221 & !q222 & !q223 & !q224 & !q225 & !q226 & !q227 & !q228 & !q229 & !q230 & !q231 & !q232 & !q233 & !q234 & !q235 & !q236 & !q237 & !q238 & !q239 & !q240 & !q241 & !q242 & !q243 & !q244 & !q245 & !q246 & !q247 & !q248 & !q249 & !q250 & !q251 & !q252 & !q253 & !q254 & !q255 & !q256 & !q257 & !q258 & !q259 & !q260 & !q261 & !q262 & !q263 & !q264 & !q265 & !q266 & !q267 & !q268 & !q269 & !q270 & !q271 & !q272 & !q273 & !q274 & !q275 & !q276 & !q277 & !q278 & !q279 & !q280 & !q281 & !q282 & !q283 & !q284 & !q285 & !q286 & !q287 & !q288 & !q289 & !q290 & !q291 & !q292 & !q293 & !q294 & !q295 & !q296 & !q297 & !q298 & !q299 & !q300 & !q301 & !q302 & !q303 & !q304 & !q305 & !q306 & !q307 & !q308 & !q309 & !q310 & !q311 & !q312 & !q313 & !q314 & !q315 & !q316 & !q317 & !q318 & !q319 & !q320 & !q321 & !q322 & !q323 & !q324 & !q325 & !q326 & !q327 & !q328 & !q329 & !q330 & !q331 & !q332 & !q333 & !q334 & !q335 & !q336 & !q337 & !q338 & !q339 & !q340 & !q341 & !q342 & !q343 & !q344 & !q345 & !q346 & !q347 & !q348 & !q349 & !q350 & !q351 & !q352 & !q353 & !q354 & !q355 & !q356 & !q357 & !q358 & !q359 & !q360 & !q361 & !q362 & !q363 & !q364 & !q365 & !q366 & !q367 & !q368 & !q369 & !q370 & !q371 & !q372 & !q373 & !q374 & !q375 & !q376 & !q377 & !q378 & !q379 & !q380 & !q381 & !q382 & !q383 & !q384 & !q385 & !q386 & !q387 & !q388 & !q389 & !q390 & !q391 & !q392 & !q393 & !q394 & !q395 & !q396 & !q397 & !q398 & !q399 & !q400 & !q401 & !q402 & !q403 & !q404 & !q405 & !q406 & !q407 & !q408 & !q409 & !q410 & !q411 & !q412 & !q413 & !q414 & !q415 & !q416 & !q417 & !q418 & !q419 & !q420 & !q421 & !q422 & !q423 & !q424 & !q425 & !q426 & !q427 & !q428 & !q429 & !q430 & !q431 & !q432 & !q433
q0 (a1 & a2 & a3 & a4 & !a5) q334
q0 (!a1 & a2 & a3 & a4 & !a5) q331
q0 (a1 & !a2 & a3 & a4 & !a5) q335
Expand Down
Loading
Loading