converting a BoolExpr to a string in SMV format

the cgi program

define y{i,k} as the output of channel i after level k; the result is a mapping of (i,k) to BoolExpr that are the case expressions defining y{i,k}

generate a map that holds the already predetermined CAS modules given by casNet and some propagation rules

read in an incomplete comparator network from a file that shall be completed to a splitter network; the file should list the levels of comparators given in brackets [] containing pairs of integers separated by ";"

determine a formula that states that exactly half of the given formulas hold; the result is a DNF of that formula (caution: exponential growth!)

generate variables g_{i,j,k} meaning there is a comparator connecting lines i and j in level k, x_{i} meaning the value of input i, and y_{i}_{k} as the output of channel i after level k

generate well-formedness constraints on the variables g{i,j,k}

This function writes the SMV file to stream ostr that states that there is no wellformed comparator network with n inputs and maximal depth d.

casMap holds already predetermined CAS modules

compute model checking problem

whether output equations shall be flattened to input variables

expand output equations by replacing their left by right hand sides

whether every channel in every level is connected by a CAS module

gVar[i].[j].[k] is an expression that holds iff channels (i,j) are connected by a CAS module in level k

whether halfOf constraint is given in DNF

constraints on inputs for splitter (conjunction implies that half of them are true)

don't print output comments, just write SMV file

whether only the final level of CAS modules may compare halves

outEqsMap map (i,k) to a pair (cLL,d) where cLL is a set of guarded actions (gs,e) such that the conjunctions of gs imply y(i,k)=e

Running NuSMV on the web server with input coming from stdin: Expected arguments are smvExe which is the path of the executable file of NuSMV like "/srv/www-es/cgi-bin/NuSMV" and a function that will write a input file for NuSMV to a stream.

whether final level of CAS network shall be a half cleaner

whether halfOf constraint shall be added (for splitter networks)

whether initial level of CAS network shall be a Parberry stage

whether there is a contraint on the number of CAS modules

wellformedness constraints (conjunction must be satisfied)

xVar[i] is an expression that denotes ith input

yVar[i].[k] is an expression that denotes ith output of level k