add storm-bn-refactoring

storm-bn-refactoring/.gitignore

+##Third-Party libs
+resources/3rdparty/l3pp/.git/
+resources/3rdparty/gtest-1.7.0/
+resources/3rdparty/gmm-5.2/
+resources/3rdparty/cudd-3.0.0/
+resources/3rdparty/xercesc-3.1.2/
+#Visual Studio files
+*.[Oo]bj
+*.user
+*.aps
+*.pch
+*.vspscc
+*.vssscc
+*_i.c
+*_p.c
+*.ncb
+*.suo
+*.tlb
+*.tlh
+*.bak
+*.[Cc]ache
+*.ilk
+*.log
+*.lib
+*.sbr
+*.sdf
+*.tlog
+*.lastbuildstate
+*.pdb
+*.idb
+*.opensdf
+*.unsuccessfulbuild
+ipch/
+obj/
+CMakeFiles/
+CPackConfig.cmake
+# The build Dir
+/*build*/
+build//CMakeLists.txt
+/*.vcxproj
+/*.filters
+/*.sln
+#Temp texteditor files
+*.orig
+*.*~
+nbproject/
+.DS_Store
+.idea
+.vscode
+*.out
+resources/3rdparty/cudd-3.0.0/Makefile.in
+resources/3rdparty/cudd-3.0.0/aclocal.m4
+# Travis helpers
+travis/mtime_cache/cache.json
+# Caroline
+CMakeCache.txt
+*.cmake
+DartConfiguration.tcl
+Makefile
+/bin/
+/googletest-prefix/
+/include/
+/l3pp_ext-prefix/
+/resources/3rdparty/
+/storm-version.cpp
+/storm.cbp

storm-bn-refactoring/CHANGELOG.md

+Changelog
+==============
+
+This changelog lists only the most important changes. Smaller (bug)fixes as well as non-mature features are not part of the changelog.
+The releases of major and minor versions contain an overview of changes since the last major/minor update.
+
+
+Version 1.6.x
+-------------
+
+## Version 1.6.3 (2020/11)
+- Added support for multi-objective model checking of long-run average objectives including mixtures with other kinds of objectives.
+- Added support for generating optimal schedulers for globally formulae
+- Simulator supports exact arithmetic
+- Added switch `--no-simplify` to disable simplification of PRISM programs (which sometimes costs a bit of time on extremely large inputs)
+- Fixed issues with JANI inputs concerning 
+    - transient variable expressions in properties,
+    - constants in properties, and
+    - integer variables with either only an upper or only a lower bound.
+- `storm-pomdp`: States can be labelled with values for observable predicates
+- `storm-pomdp`: (Only API) Track state estimates
+- `storm-pomdp`: (Only API) Reduce computation of state estimates to computation on unrolled MDP
+
+## Version 1.6.2 (2020/09)
+- Prism program simplification improved.
+- Revamped implementation of long-run-average algorithms, including scheduler export for LRA properties on Markov automata.
+- Support for step-bounded properties of the form ... [F[x,y] ... ] for DTMCs and MDPs (sparse engine).
+- Renamed portfolio engine to automatic 
+- `storm-dft`: Fix for relevant events when using symmetry reduction.
+- `storm-pomdp`: Fix for --transformsimple and --transformbinary when used with until formulae.
+- `storm-pomdp`: POMDPs can be parametric as well.
+
+## Version 1.6.0 (2020/06)
+- Changed default Dd library from `cudd` to `sylvan`. The Dd library can be changed back to `cudd` using the command line switch `--ddlib`.
+- Scheduler export: Properly handle models with end components. Added export in `.json` format.
+- CMake: Search for Gurobi prefers new versions.
+- CMake: We no longer ship xerces-c. If xerces-c is not found on the system, storm-gspn will not be able to parse xml-based GSPN formats.
+- CMake: Added option `STORM_LOAD_QVBS` to automatically download the quantitative verification benchmark set.
+- Eigen library: The source code of Eigen is no longer included but downloaded from an external repository instead. Incremented Eigen version to 3.3.7 which fixes a compilation issue with recent XCode versions.
+- Tests: Enabled tests for permissive schedulers.
+- `storm-counterexamples`: fix when computing multiple counterexamples in debug mode.
+- `storm-dft`: Renamed setting `--show-dft-stats` to `dft-statistics` and added approximation information to statistics.
+- `storm-pomdp`: Implemented approximation algorithms that explore (a discritization of) the belief MDP, allowing to compute safe lower- and upper bounds for a given property.
+- `storm-pomdp`: Implemented almost-sure reachability computations: graph-based, one-shot SAT-based, and iterative SAT-based.
+- `storm-pomdp': Various changes such that transformation to pMCs is now again supported (and improved).
+- Fixed several compiler warnings.
+
+
+Version 1.5.x
+-------------
+
+## Version 1.5.1 (2020/03)
+- Jani models are now parsed using exact arithmetic.
+
+## Version 1.5.0 (2020/03)
+- Added portfolio engine which picks a good engine (among other settings) based on features of the symbolic input.
+- Abort of Storm (via timeout or CTRL+C for example) is now gracefully handled. After an abort signal the program waits some seconds to output the result computed so far and terminates afterwards. A second signal immediately terminates the program.
+- Setting `--engine dd-to-sparse --bisimulation` now triggers extracting the sparse bisimulation quotient.
+- JIT model building is now invoked via `--engine jit` (instead of `--jit`).
+- DRN: support import of choice labelling.
+- Added option `--build:buildchoiceorig` to build a model (PRISM or JANI) with choice origins (which are exported with, e.g. `--exportscheduler`).
+- Implemented optimistic value iteration for sound computations and set it as new default in `--sound` mode.
+- Time bounded properties for Markov automata are now computed with relative precision. Use `--absolute` for the previous behavior.
+- Apply the maximum progress assumption while building a Markov automaton with one of the symbolic engines.
+- Added option `--build:nomaxprog` to disable applying the maximum progress assumption during model building (for Markov Automata).
+- Added hybrid engine for Markov Automata.
+- Improved performance of the Unif+ algorithm (used for time-bounded properties on Markov Automata).
+- Various performance improvements for model building with the sparse engine.
+- `storm-dft`: Symmetry reduction is now enabled by default and can be disabled via `--nosymmetryreduction`.
+- `storm-pomdp`: Only accept POMDPs that are canonical.
+- `storm-pomdp`: Prism language extended with observable expressions.
+- `storm-pomdp`: Various fixes that prevented usage.
+- Several bug fixes.
+
+
+Version 1.4.x
+-------------
+
+### Version 1.4.1 (2019/12)
+- Implemented long run average (LRA) computation for DTMCs/CTMCs via value iteration and via gain/bias equations.
+- Added several LRA related settings in a new settings module. Note that `--minmax:lramethod` has been replaced by `--lra:nondetmethod`.
+
+### Version 1.4.0 (2019/11)
+- Added support for multi-dimensional quantile queries.
+- Added support for multi-objective model checking under pure (deterministic) schedulers with bounded memory using `--purescheds`.
+- Allow to quickly check a benchmark from the [Quantitative Verification Benchmark Set](http://qcomp.org/benchmarks/) using the `--qvbs` option.
+- Added script `resources/examples/download_qvbs.sh` to download the QVBS.
+- If an option is unknown, Storm now suggests similar option names.
+- Flagged several options as 'advanced' to clean up the `--help`-message. Use `--help all` to display a complete list of options.
+- Support for parsing of exact time bounds for properties, e.g., `P=? [F=27 "goal"]`.
+- Export of optimal schedulers when checking MDPs with the sparse engine (experimental). Use  `--exportscheduler <filename>`.
+- PRISM language: Support for the new `round` operator.
+- PRISM language: Improved error messages of the parser.
+- JANI: Allow bounded types for constants.
+- JANI: Support for non-trivial reward accumulations.
+- JANI: Fixed support for reward expressions over non-transient variables.
+- DRN: Added support for exact parsing and action-based rewards.
+- DRN: Support for placeholder variables which allows to parse recurring rational functions only once.
+- Fixed sparse bisimulation of MDPs (which failed if all non-absorbing states in the quotient are initial).
+- Support for export of MTBDDs from Storm.
+- Support for k-shortest path counterexamples (arguments `-cex --cextype shortestpath`)
+- New settings module `transformation` for Markov chain transformations. Use `--help transformation` to get a list of available transformations.
+- Support for eliminating chains of Non-Markovian states in MAs via `--eliminate-chains`.
+- Export to dot format allows for maximal line width in states (argument `--dot-maxwidth <width>`)
+- `storm-conv` can now apply transformations on a prism file.
+- `storm-pars`: Enabled building, bisimulation and analysis of symbolic models.
+- `storm-dft`: Support partial-order for state space generation.
+- `storm-dft`: Compute lower and upper bounds for number of BE failures via SMT.
+- `storm-dft`: Allow to set relevant events which are not set to Don't Care.
+- `storm-dft`: Support for constant failed BEs. Use flag `--uniquefailedbe` to create a unique constant failed BE.
+- `storm-dft`: Support for probabilistic BEs via PDEPs.
+- Fixed linking with Mathsat on macOS.
+- Fixed linking with IntelTBB for GCC.
+- Fixed compilation for macOS Mojave and higher.
+- Several bug fixes.
+
+
+Version 1.3.x
+-------------
+
+## Version 1.3.0 (2018/12)
+- Slightly improved scheduler extraction
+- Environments are now part of the c++ API
+- Heavily extended JANI support, in particular:
+	 * arrays, functions, state-exit-rewards (all engines)
+	 * indexed assignments, complex reward expressions (sparse engine)
+	 * several jani-related bug fixes
+- New binary `storm-conv` that handles conversions between model files
+- New binary `storm-pomdp` that handles the translation of POMDPs to pMCs.
+- Maximal progress assumption is now applied while building Markov Automata (sparse engine).
+- Improved Unif+ implementation for Markov Automata, significantly reduced memory consumption.
+- Added support for expected time properties for discrete time models
+- Bug fix in the parser for DRN (MDPs and MAs might have been affected).
+- `storm-gspn`: Improved .pnpro parser
+- `storm-gspn`: Added support for single/infinite/k-server semantics for GSPNs given in the .pnpro format
+- `storm-gspn`: Added option to set a global capacity for all places
+- `storm-gspn`: Added option to include a set of standard properties when converting GSPNs to jani
+- `storm-pars`: Added possibility to compute the extremal value within a given region using parameter lifting
+- `storm-dft`: DFT translation to GSPN supports Don't Care propagation
+- `storm-dft`: Support DFT analysis via transformation from DFT to GSPN to JANI
+- `storm-dft`: Added SMT encoding for DFTs
+- `storm-dft`: Improved Galileo and JSON parser
+- Several bug fixes
+- Storm uses the `master14` branch of carl from now on
+
+### Comparison with Version 1.2.0 (details see below)
+- Heavily extended JANI-support
+- New binary `storm-conv` that handles conversion between model files
+- New binary `storm-pomdp` that  handles the translation of POMDPs to pMCs.
+- `storm-gspn` improved
+- Sound value iteration
+
+
+Version 1.2.x
+-------------
+
+### Version 1.2.3 (2018/07)
+- Fix in version parsing
+
+### Version 1.2.2 (2018/07)
+- Sound value iteration (SVI) for DTMCs and MDPs
+- Topological solver for linear equation systems and MinMax equation systems (enabled by default)
+- Added support for expected total rewards in the sparse engine
+- By default, iteration-based solvers are no longer aborted after a given number of steps.
+- Improved export for jani models
+- A fix in parsing jani properties
+- Several extensions to high-level counterexamples
+- `storm-parsers` extracted to reduce linking time
+- `storm-counterexamples` extracted to reduce linking time
+- `storm-dft`: improvements in Galileo parser
+- `storm-dft`: test cases for DFT analysis
+- Improved Storm installation
+- Several bug fixes
+
+### Version 1.2.1 (2018/02)
+- Multi-dimensional reward bounded reachability properties for DTMCs.
+- `storm-dft`: transformation of DFTs to GSPNs
+- Several bug fixes
+
+### Version 1.2.0 (2017/12)
+- C++ api changes: Building model takes `BuilderOptions` instead of extended list of Booleans, does not depend on settings anymore.
+- `storm-cli-utilities` now contains cli related stuff, instead of `storm-lib`
+- Symbolic (MT/BDD) bisimulation
+- Fixed issue related to variable names that can not be used in Exprtk.
+- DRN parser improved
+- LP-based MDP model checking
+- Sound (interval) value iteration
+- Support for Multi-objective multi-dimensional reward bounded reachability properties for MDPs.
+- RationalSearch method to solve equation systems exactly
+- WalkerChae method for solving linear equation systems with guaranteed convergence
+- Performance improvements for sparse model building
+- Performance improvements for conditional properties on MDPs
+- Automatically convert MA without probabilistic states into CTMC
+- Fixed implemention of Fox and Glynn' algorithm
+- `storm-pars`: support for welldefinedness constraints in mdps.
+- `storm-dft`: split DFT settings into IO settings and fault tree settings
+- `storm-dft`: removed obsolete explicit model builder for DFTs
+- Features for developers:
+	* Solvers can now expose requirements
+	* unbounded reachability and reachability rewards now correctly respect solver requirements
+	* Environment variables (such as the solver precisions) can now be handled more flexible
+	* changes to Matrix-Vector operation interfaces, in particular fixed some issues with the use Intel TBB
+
+
+Version 1.1.x
+-------------
+
+### Version 1.1.0 (2017/8)
+- Support for long-run average rewards on MDPs and Markov automata using a value-iteration based approach.
+- Storm can now check MDPs and Markov Automata (i.e. MinMax equation systems) via Linear Programming.
+- Parametric model checking is now handled in a separated library/executable called `storm-pars`.
+- Wellformedness constraints on PMCs:
+    * include constraints from rewards
+    * are in smtlib2
+    * fixed
+    * computation of only constraints without doing model checking is now supported
+- Fix for nested formulae
+- JANI: Explicit engine supports custom model compositions.
+- Support for parsing/building models given in the explicit input format of IMCA.
+- Storm now overwrites files if asked to write files to a specific location.
+- Changes in build process to accommodate for changes in carl. Also, more robust against issues with carl.
+- `USE_POPCNT` removed in favor of `FORCE_POPCNT`. The popcnt instruction is used if available due to `march=native`, unless portable is set.
+  Then, using `FORCE_POPCNT` enables the use of the SSE 4.2 instruction
+
+
+Version 1.0.x
+-------------
+
+### Version 1.0.1 (2017/4)
+- Multi-objective model checking support now fully included
+- Several improvements in parameter lifting
+- Several improvements in JANI parsing
+- Properties can contain model variables
+- Support for rational numbers/functions in decision diagrams via sylvan
+- Elimination-based solvers (exact solution) for models stored as decision diagrams
+- Export of version and configuration to cmake
+- Improved building process
+
+### Version 1.0.0 (2017/3)
+Start of this changelog

storm-bn-refactoring/README.md

+# Storm-bn-refactoring
+
+
+
+
+[![Build Status](https://travis-ci.org/joemccann/dillinger.svg?branch=master)](https://travis-ci.org/joemccann/dillinger)
+
+A tool that transforms a (parametric) Bayesian network (pBN) to their corresponding (parametric) Markov chain (pMC). This is done to reduce inference in pBNs to probabilistic inference in pMCs.
+
+## Installation
+[Storm]
+## Installation
+
+
+```sh
+cd storm-bn-refactoring
+mkdir build && cd build
+cmake ..
+make storm-bn-robin
+```
+
+
+## Run
+
+```
+./path-to- storm-bn-refactoring-directory/build/bin/storm-bn-robin network_name
+```
+- 'network_name': the name of the network you want to transform to a (p)MC.
+- 'path-to- storm-bn-refactoring-directory': the path to the directory where storm-bn-refactoring was installed.
+
+
+## License
+RWTH Aachen University

storm-bn-refactoring/cuda/CMakeAlignmentCheck.cpp

+/*
+ * This is component of StoRM - Cuda Plugin to check whether type alignment matches the assumptions done while optimizing the code.
+ */
+ #include <cstdint>
+ #include <utility>
+ #include <vector>
+ 
+ #define CONTAINER_SIZE 100ul
+ 
+ template <typename IndexType, typename ValueType>
+ int checkForAlignmentOfPairTypes(size_t containerSize, IndexType const firstValue, ValueType const secondValue) {
+	std::vector<std::pair<IndexType, ValueType>>* myVector = new std::vector<std::pair<IndexType, ValueType>>();
+	for (size_t i = 0; i < containerSize; ++i) {
+		myVector->push_back(std::make_pair(firstValue, secondValue));
+	}
+	size_t myVectorSize = myVector->size();
+	IndexType* firstStart = &(myVector->at(0).first);
+	IndexType* firstEnd = &(myVector->at(myVectorSize - 1).first);
+	ValueType* secondStart = &(myVector->at(0).second);
+	ValueType* secondEnd = &(myVector->at(myVectorSize - 1).second);
+	size_t startOffset = reinterpret_cast<size_t>(secondStart) - reinterpret_cast<size_t>(firstStart);
+	size_t endOffset = reinterpret_cast<size_t>(secondEnd) - reinterpret_cast<size_t>(firstEnd);
+	size_t firstOffset = reinterpret_cast<size_t>(firstEnd) - reinterpret_cast<size_t>(firstStart);
+	size_t secondOffset = reinterpret_cast<size_t>(secondEnd) - reinterpret_cast<size_t>(secondStart);
+	
+	delete myVector;
+	myVector = nullptr;
+	
+	if (myVectorSize != containerSize) {
+		return -2;
+	}
+	
+	// Check for alignment:
+	// Requirement is that the pairs are aligned like: first, second, first, second, first, second, ...
+	if (sizeof(IndexType) != sizeof(ValueType)) {
+		return -3;
+	}
+	if (startOffset != sizeof(IndexType)) {
+		return -4;
+	}
+	if (endOffset != sizeof(IndexType)) {
+		return -5;
+	}
+	if (firstOffset != ((sizeof(IndexType) + sizeof(ValueType)) * (myVectorSize - 1))) {
+		return -6;
+	}
+	if (secondOffset != ((sizeof(IndexType) + sizeof(ValueType)) * (myVectorSize - 1))) {
+		return -7;
+	}
+	
+	return 0;
+ }
+ 
+ 
+ int main(int argc, char* argv[]) {
+	int result = 0;
+	
+	result = checkForAlignmentOfPairTypes<uint_fast64_t, double>(CONTAINER_SIZE, 42, 3.14);
+	if (result != 0) {
+		return result;
+	}
+	
+	return 0;
+ }

storm-bn-refactoring/cuda/CMakeFloatAlignmentCheck.cpp

+/*
+ * This is component of StoRM - Cuda Plugin to check whether a pair of uint_fast64_t and float gets auto-aligned to match 64bit boundaries
+ */
+ #include <cstdint>
+ #include <utility>
+ #include <vector>
+ 
+ #define CONTAINER_SIZE 100ul
+
+int main(int argc, char* argv[]) {
+	int result = 0;
+
+	std::vector<std::pair<uint_fast64_t, float>> myVector;
+	for (size_t i = 0; i < CONTAINER_SIZE; ++i) {
+		myVector.push_back(std::make_pair(i, 42.12345f * i));
+	}
+	
+	char* firstUintPointer = reinterpret_cast<char*>(&(myVector.at(0).first));
+	char* secondUintPointer = reinterpret_cast<char*>(&(myVector.at(1).first));
+	ptrdiff_t uintDiff = secondUintPointer - firstUintPointer;
+	
+	if (uintDiff == (2 * sizeof(uint_fast64_t))) {
+		result = 2;
+	} else if (uintDiff == (sizeof(uint_fast64_t) + sizeof(float))) {
+		result = 3;
+	} else {
+		result = -5;
+	}
+	
+	return result;
+ }

storm-bn-refactoring/cuda/kernels/allCudaKernels.h

+#include "utility.h"
+#include "bandWidth.h"
+#include "basicAdd.h"
+#include "kernelSwitchTest.h"
+#include "basicValueIteration.h"
+#include "version.h"
\ No newline at end of file

storm-bn-refactoring/cuda/kernels/basicAdd.cu

+#include <cuda.h>
+#include <stdlib.h>
+#include <stdio.h>
+
+#include <chrono>
+#include <iostream>
+
+__global__ void cuda_kernel_basicAdd(int a, int b, int *c) { 
+	*c = a + b; 
+}
+
+__global__ void cuda_kernel_arrayFma(int const * const A, int const * const B, int const * const C, int * const D, int const N) {
+	// Fused Multiply Add:
+	// A * B + C => D
+
+	/*
+     *Die Variable i dient fr den Zugriff auf das Array. Da jeder Thread die Funktion VecAdd
+     *ausfhrt, muss i fr jeden Thread unterschiedlich sein. Ansonsten wrden unterschiedliche
+     *Threads auf denselben Index im Array schreiben. blockDim.x ist die Anzahl der Threads der x-Komponente
+     *des Blocks, blockIdx.x ist die x-Koordinate des aktuellen Blocks und threadIdx.x ist die x-Koordinate des
+     *Threads, der die Funktion gerade ausfhrt.
+    */
+    int i = blockDim.x * blockIdx.x + threadIdx.x;
+
+	if (i < N) {
+		D[i] = A[i] * B[i] + C[i];
+	}
+}
+
+__global__ void cuda_kernel_arrayFmaOptimized(int * const A, int const N, int const M) {
+	// Fused Multiply Add:
+	// A * B + C => D
+
+	// Layout:
+	// A B C D A B C D A B C D
+
+    int i = blockDim.x * blockIdx.x + threadIdx.x;
+
+	if ((i*M) < N) {
+		for (int j = i*M; j < i*M + M; ++j) {
+			A[j*4 + 3] = A[j*4] * A[j*4 + 1] + A[j*4 + 2];
+		}
+	}
+}
+
+extern "C" int cuda_basicAdd(int a, int b) {
+	int c = 0;
+	int *dev_c;
+	cudaMalloc((void**)&dev_c, sizeof(int));
+	cuda_kernel_basicAdd<<<1, 1>>>(a, b, dev_c);
+	cudaMemcpy(&c, dev_c, sizeof(int), cudaMemcpyDeviceToHost);
+	//printf("%d + %d + 42 is %d\n", a, b, c);
+	cudaFree(dev_c);
+	return c;
+}
+
+void cpp_cuda_bandwidthTest(int entryCount, int N) {
+	// Size of the Arrays
+	size_t arraySize = entryCount * sizeof(int);
+	
+	int* deviceIntArray;
+	int* hostIntArray = new int[arraySize];
+
+	// Allocate space on the device
+	auto start_time = std::chrono::high_resolution_clock::now();
+	for (int i = 0; i < N; ++i) {
+		if (cudaMalloc((void**)&deviceIntArray, arraySize) != cudaSuccess) {
+			std::cout << "Error in cudaMalloc while allocating " << arraySize << " Bytes!" << std::endl;
+			delete[] hostIntArray;
+			return;
+		}
+		// Free memory on device
+		if (cudaFree(deviceIntArray) != cudaSuccess) {
+			std::cout << "Error in cudaFree!" << std::endl;
+			delete[] hostIntArray;
+			return;
+		}
+	}
+	auto end_time = std::chrono::high_resolution_clock::now();
+	auto copyTime = std::chrono::duration_cast<std::chrono::microseconds>(end_time - start_time).count();
+	double mBytesPerSecond = (((double)(N * arraySize)) / copyTime) * 0.95367431640625;
+	std::cout << "Allocating the Array " << N << " times took " << copyTime << " Microseconds." << std::endl;
+	std::cout << "Resulting in " << mBytesPerSecond << " MBytes per Second Allocationspeed." << std::endl;
+
+	if (cudaMalloc((void**)&deviceIntArray, arraySize) != cudaSuccess) {
+		std::cout << "Error in cudaMalloc while allocating " << arraySize << " Bytes for copyTest!" << std::endl;
+		delete[] hostIntArray;
+		return;
+	}
+	
+	// Prepare data
+	for (int i = 0; i < N; ++i) {
+		hostIntArray[i] = i * 333 + 123;
+	}
+
+	// Copy data TO device
+	start_time = std::chrono::high_resolution_clock::now();
+	for (int i = 0; i < N; ++i) {
+		if (cudaMemcpy(deviceIntArray, hostIntArray, arraySize, cudaMemcpyHostToDevice) != cudaSuccess) {
+			std::cout << "Error in cudaMemcpy while copying " << arraySize << " Bytes to device!" << std::endl;
+			// Free memory on device
+			if (cudaFree(deviceIntArray) != cudaSuccess) {
+				std::cout << "Error in cudaFree!" << std::endl;
+			}
+			delete[] hostIntArray;
+			return;
+		}
+	}
+	end_time = std::chrono::high_resolution_clock::now();
+	copyTime = std::chrono::duration_cast<std::chrono::microseconds>(end_time - start_time).count();
+	mBytesPerSecond = (((double)(N * arraySize)) / copyTime) * 0.95367431640625;
+	std::cout << "Copying the Array " << N << " times took " << copyTime << " Microseconds." << std::endl;
+	std::cout << "Resulting in " << mBytesPerSecond << " MBytes per Second TO device." << std::endl;
+
+	// Copy data FROM device
+	start_time = std::chrono::high_resolution_clock::now();
+	for (int i = 0; i < N; ++i) {
+		if (cudaMemcpy(hostIntArray, deviceIntArray, arraySize, cudaMemcpyDeviceToHost) != cudaSuccess) {
+			std::cout << "Error in cudaMemcpy while copying " << arraySize << " Bytes to host!" << std::endl;
+			// Free memory on device
+			if (cudaFree(deviceIntArray) != cudaSuccess) {
+				std::cout << "Error in cudaFree!" << std::endl;
+			}
+			delete[] hostIntArray;
+			return;
+		}
+	}
+	end_time = std::chrono::high_resolution_clock::now();
+	copyTime = std::chrono::duration_cast<std::chrono::microseconds>(end_time - start_time).count();
+	mBytesPerSecond = (((double)(N * arraySize)) / copyTime) * 0.95367431640625;
+	std::cout << "Copying the Array " << N << " times took " << copyTime << " Microseconds." << std::endl;
+	std::cout << "Resulting in " << mBytesPerSecond << " MBytes per Second FROM device." << std::endl;
+
+	// Free memory on device
+	if (cudaFree(deviceIntArray) != cudaSuccess) {
+		std::cout << "Error in cudaFree!" << std::endl;
+	}
+	delete[] hostIntArray;
+}
+
+extern "C" void cuda_arrayFma(int const * const A, int const * const B, int const * const C, int * const D, int const N) {
+	// Size of the Arrays
+	size_t arraySize = N * sizeof(int);
+	
+