Skip to content

Commit

Permalink
Merge branch 'develop'
Browse files Browse the repository at this point in the history
  • Loading branch information
HannesK committed Feb 27, 2017
2 parents e097504 + 4f38916 commit 3302f66
Show file tree
Hide file tree
Showing 291 changed files with 540,931 additions and 607 deletions.
Binary file not shown.
8 changes: 8 additions & 0 deletions Dependencies/linux32/BNetToPrime/CMakeLists.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
cmake_minimum_required (VERSION 2.4)
PROJECT(BNetToPrime)

# Target
FILE(GLOB MY_HEADERS ${BNetToPrime_SOURCE_DIR}/source/*.h)
ADD_EXECUTABLE(BNetToPrime main.cpp ${MY_HEADERS})


100 changes: 100 additions & 0 deletions Dependencies/linux32/BNetToPrime/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,100 @@
# BNetToPrime

This tool converts a Boolean Network in the BoolNet format to a list of all prime implicants for each regulatory function.

### Compiling
Extra easy to compile:
```shell
cd BNetToPrime
"compiler" main.cpp
```
where "compiler" is either g++ on Unix/Linux, clang++ on MacOS, or cl on Windows.

A binary file gets produced based on the platform (e.g. a.out on Unix/Linux).

The code is C++98 compliant.
### Running
```shell
BNetToPrime [--help][--ver][input [output]]
--help displays help
--ver displays version
input the path to the input file, if missing, the standard input (console/terminal) is used
output the path to the output file, if missing, the standard output is used
```
### Input file
Each line input file is expected to be of the form:
```
target, function
```
where "target" is a name of a component and "function" is a boolean function over components with "&" for conjunction, "|" for disjunction, "!" for negation.
Note, if the line is "targets, factors" (as a result of printing it from BoolNet) then it is ignored.
### Output file
Output is a json object that holds for each component an array with two elements.
The first element is a list of all prime implicants of the negation of its regulatory function.
The second element is a list of all prime implicants of its regulatory function.
If the component appears only in a function, a new line with 'component,component' is added.
An empty list means there is no implicant, i.e. the function is not satisfiable.
A list with only an empty object means that the formula is tautology, i.e. it is always satisfiable.
### Example
#### Input
```
targets, factors
A, B & C
B, !A | B
```
#### Output (formatted with whitespace)
```
{
"A": [
[
{
"C": 0
},
{
"B": 0
}
],
[
{
"B": 1,
"C": 1
}
]
],
"B": [
[
{
"A": 1,
"B": 0
}
],
[
{
"B": 1
},
{
"A": 0
}
]
],
"C": [
[
{
"C": 0
}
],
[
{
"C": 1
}
]
]
}
```
177 changes: 177 additions & 0 deletions Dependencies/linux32/BNetToPrime/main.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,177 @@
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// @brief The BNetToPrime program that converts a Boolean Network to a list of prime implicants for all the regulatory functions.
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////

#include "source/formulae_resolver.h"
#include "source/implicant_enumerator.h"

bool has_fin;
bool has_fout;

// #define RUN_TESTS


// @brief The number of the regulators is bounded by the nubmer of bits in the size_t
size_t maxRegulatorsCount() {
return sizeof(size_t) * 8;
}

// @brief from the id obtain the valation of the respective variables (e.g. for id==4 and variables=={A,B,C} we get (A=1,B=0,C=0), for id==1 we get (A=0,B=0,C=1))
Minterm valuationToVals(const size_t valuation_id, map<string, bool> & valuation) {
Minterm result(valuation.size(), 0);
int ele = 0;
for (map<string, bool>::iterator it = valuation.begin(); it != valuation.end(); it++, ele++) {
bool val = ((valuation_id >> (valuation.size() - 1 - ele)) % 2) == 1;
result[ele] = val;
it->second = val;
}
return result;
}

// @brief if # is present, remove everything after it
string removeComment(const string & original) {
const size_t pos = original.find('#');
return original.substr(0, pos);
}

//
int main(int argc, char ** argv) {
try {
#ifdef _MSC_VER //Set the output buffer size for visual studio
setvbuf(stdout, 0, _IOLBF, 4096);
#endif
#ifdef RUN_TESTS
FormulaeResolver::test();
#else
// Parse the input
if (argc > 1) {
string arg1 = argv[1];
if (arg1 == "--help" || arg1 == "-h") {
IO::printHelp();
return 0;
}
if (arg1 == "--ver" || arg1 == "-v") {
IO::printVersion();
return 0;
}
}
has_fin = argc > 1;
has_fout = argc > 2;

// Open the input and output files, use standard streams if not specified
fstream fin;
if (has_fin) {
fin.open(argv[1], fstream::in);
if (!fin) {
throw invalid_argument(string("Failed to open the input file ") + argv[1]);
}
}
istream & in = has_fin ? fin : cin;

fstream fout;
if (has_fout) {
fout.open(argv[2], fstream::out);
if (!fout) {
throw invalid_argument(string("Failed to open the output file ") + argv[2]);
}
}
ostream & out = has_fout ? fout : cout;


// Holds the input
map<string, pair<vector<string>, string> > line_data;
string line;
// Read computed and write line by line
while (getline(in, line)) {
line = FormulaeResolver::removeWhitespaces(line);
line = removeComment(line);
// Skip the first line, if it is "targets,factors"
if (line.empty() || line == "targets,factors" ) {
continue;
}
// Parse the line
size_t comma_pos = line.find(',');
string component = line.substr(0, comma_pos);
if (line_data.count(component)) {
throw runtime_error(component + " already has a function.");
}
string formula = FormulaeResolver::removeWhitespaces(line.substr(comma_pos + 1));
vector<string> regulators = IO::getAllRegulators(formula);
line_data.insert(make_pair(component, make_pair(regulators, formula)));
}

// Check if all components are present, if not, add self-regulation
for (map<string, pair<vector<string>, string> >::iterator it = line_data.begin(); it != line_data.end(); it++) {
for (vector<string>::const_iterator comp_it = it->second.first.begin(); comp_it != it->second.first.end(); comp_it++) {
if (line_data.count(*comp_it) == 0) {
vector<string> regulators;
regulators.push_back(*comp_it);
line_data.insert(make_pair(*comp_it, make_pair(regulators, *comp_it)));
}
}
}

// Compute and output data for each line
out << "{";
for (map<string, pair<vector<string>, string> >::const_iterator it = line_data.begin(); it != line_data.end(); it++) {
const string component = it->first;
const vector<string> regulators = it->second.first;
const string formula = it->second.second;

const size_t VALUATIONS_COUNT = static_cast<size_t>(pow(2, regulators.size())); // How many valuations of the variables there are
if (regulators.size() > maxRegulatorsCount()) {
throw runtime_error("The component '" + component + "' has too many regulators.");
}

// Create the valuation map, also write the current line on the output
map<string, bool> valuation;
IF_HAS_FOUT(cout << "\rTarget: '" << component << "'. Regulators: [";)
for (vector<string>::const_iterator it = regulators.begin(); it != regulators.end(); it++) {
IF_HAS_FOUT(cout << *it << ",";)
valuation.insert(make_pair(*it, false));
}
IF_HAS_FOUT(cout << "]" << endl;)

// Resolve the formulas and push the values to the respective vectors
DNF true_elems;
DNF false_elems;
for (size_t valuation_id = 0; valuation_id < VALUATIONS_COUNT; valuation_id++) {
Minterm new_elem = valuationToVals(valuation_id, valuation);
if (FormulaeResolver::resolve(valuation, formula)) {
true_elems.push_back(new_elem);
}
else {
false_elems.push_back(new_elem);
}
IF_HAS_FOUT(cout << "\rSolving formula: " << valuation_id + 1 << "/" << VALUATIONS_COUNT;)
}

// Compactize and write the output immediatelly
out << "\"" << component << "\":[";
IF_HAS_FOUT(cout << "\r\tComputing implicants for: '!(" << formula << ")'\n";)
ImplicantEnumerator::compactize(regulators.size(), false_elems);
IO::printDNF(false_elems, regulators, out);
false_elems.clear();
out << ",";
IF_HAS_FOUT(cout << "\r\tComputing implicants for: '" << formula << "'\n";)
ImplicantEnumerator::compactize(regulators.size(), true_elems);
IO::printDNF(true_elems, regulators, out);
true_elems.clear();
out << "],";
}

// Remove the last comma
if (!line_data.empty()) {
REMOVE_LAST
}
out << "}" << std::endl << flush;
#endif
}
catch (exception & e) {
cerr << PROGRAM_NAME << " encountered an exception and aborted." << endl;
cerr << "Exception message: \"" << e.what() << "\"" << endl;
return 1;
}

return 0;
}
Binary file added Dependencies/linux32/NuSMV-a/NuSMVa_linux32
Binary file not shown.
Binary file added Dependencies/linux32/NuSMV-a/ltl2smv
Binary file not shown.
Loading

0 comments on commit 3302f66

Please sign in to comment.