Merge dev branch

.gitignore

@@ -3,6 +3,7 @@ build
 bin
 tmp
 doxysite
+release
 storm
 *.o
 *.out
@@ -28,3 +29,9 @@ ecm_uninstall.cmake
 *_autogen
 prefix.sh
 
+# Third party icons
+src/stamina/gui/resources/*icons*
+
+# Distribution stuff
+PKGBUILD
+AppImageBuilder.yml

CMakeLists.txt

@@ -5,26 +5,24 @@
 ##
 
 cmake_minimum_required(VERSION 3.10)
-project(stamina)			   # Create project "stamina"
+# Create project "stamina"
+project(stamina)
 set(LIB_NAME stamina)
 set(CLI_EXECUTABLE_NAME sstamina)
-set(CMAKE_CXX_STANDARD 17)			# Enable c++17 standard
+# Enable c++17 standard
+set(CMAKE_CXX_STANDARD 20)
 set(CMAKE_CXX_STANDARD_REQUIRED True)
 
+if (${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
+    set(MACOSX TRUE)
+endif()
+
 option(STAMINA_DEBUG "Include debug information in the executables" OFF)
 if (STAMINA_DEBUG)
 	set(CMAKE_BUILD_TYPE Debug)
 endif()
 
-# STAMINA Build
-# option(STAMINA_BUILD_TAG "Build tag information" "unspecified")
-execute_process(
-	COMMAND git rev-parse HEAD
-	WORKING_DIRECTORY ${CMAKE_CURRENT_LIST_DIR}
-	OUTPUT_VARIABLE GIT_HASH
-	OUTPUT_STRIP_TRAILING_WHITESPACE
-)
-add_compile_definitions(STAMINA_BUILD_INFO="Debug Build")
+include(StaminaVersion.cmake)
 
 # Build options
 option(BUILD_GUI "Build XStamina GUI" OFF)
@@ -49,15 +47,15 @@ if (BUILD_GUI)
 	find_package(KF5TextEditor)
 
 	find_package(Qt5 ${QT_MIN_VERSION} CONFIG REQUIRED COMPONENTS
-		Core	# QCommandLineParser, QStringLiteral
-		Widgets # QApplication
+		Core         # QCommandLineParser, QStringLiteral
+		Widgets      # QApplication
 	)
 
 	find_package(KF5 ${KF5_MIN_VERSION} REQUIRED COMPONENTS
-		CoreAddons	  # KAboutData
-		I18n			# KLocalizedString
-		XmlGui		  # KXmlGuiWindow
-		TextWidgets	 # KTextEdit
+		CoreAddons        # KAboutData
+		I18n              # KLocalizedString
+		XmlGui            # KXmlGuiWindow
+		TextWidgets       # KTextEdit
 	)
 	find_package(KF5KIO)
 
@@ -138,6 +136,7 @@ set(UIC_UI_FILES
 
 set(GUI_RECS
 	${GUI_PREFIX}/resources.qrc
+	${GUI_PREFIX}/icons.qrc
 )
 
 option(STAMINA_BUILD_STORM "Build Storm in this directory and package with STAMINA" OFF)
@@ -205,12 +204,21 @@ endif()
 
 # Install stuff
 # install(TARGETS ${PROJECT_NAME} RUNTIME DESTINATION bin)
+# MacOS requires a MACOSX_BUNDLE setting
 if (BUILD_GUI)
-	install(TARGETS ${GUI_EXECUTABLE_NAME} RUNTIME DESTINATION bin COMPONENT applications)
+	install(TARGETS ${GUI_EXECUTABLE_NAME} RUNTIME DESTINATION bin BUNDLE DESTINATION bin COMPONENT applications)
 endif()
+install(TARGETS ${CLI_EXECUTABLE_NAME} RUNTIME DESTINATION bin BUNDLE DESTINATION  bin COMPONENT applications)
 
-install(TARGETS ${CLI_EXECUTABLE_NAME} RUNTIME DESTINATION bin COMPONENT applications)
 # This installs libstamina
-install(TARGETS ${LIB_NAME} RUNTIME DESTINATION lib COMPONENT libraries)
+install(TARGETS ${LIB_NAME} RUNTIME DESTINATION lib BUNDLE DESTINATION  lib COMPONENT libraries)
 
 include(StaminaCPackConfig.cmake)
+
+# Tests are not included in packaging
+
+option(STAMINA_BUILD_TESTS "Build STAMINA unit tests" OFF)
+
+if (STAMINA_BUILD_TESTS)
+	include(test/unit/CMakeLists.txt)
+endif()

Dockerfile

@@ -1,6 +1,6 @@
-from movesrwth/storm:ci-release
+from movesrwth/storm:ci
 
-RUN apt-get update && apt-get install -y build-essential libboost-all-dev git cmake clang 
+RUN apt-get update && apt-get install -y build-essential libboost-all-dev git cmake clang
 RUN apt-get install git
 
 ENV STORM_DIR=/opt/storm

StaminaCPackConfig.cmake

@@ -1,6 +1,5 @@
 option(BUILD_CPACK "Creates/includes CPack file" Off)
 if (BUILD_CPACK)
-
 	set(CPACK_PACKAGE_VERSION_MAJOR "0")
 	set(CPACK_PACKAGE_VERSION_MINOR "2")
 	set(CPACK_PACKAGE_VERSION_PATCH "5")

StaminaVersion.cmake

@@ -0,0 +1,24 @@
+set(STAMINA_VERSION_MAJOR "0")
+set(STAMINA_VERSION_MINOR "2")
+set(STAMINA_VERSION_PATCH "5")
+
+# STAMINA Build
+# option(STAMINA_BUILD_TAG "Build tag information" "unspecified")
+option(STAMINA_INCLUDE_GIT_BUILD_INFO "Includes git tag information in build info" Off)
+if (STAMINA_INCLUDE_GIT_BUILD_INFO)
+	execute_process(
+		COMMAND git rev-parse HEAD
+		WORKING_DIRECTORY ${CMAKE_CURRENT_LIST_DIR}
+		OUTPUT_VARIABLE GIT_HASH
+		OUTPUT_STRIP_TRAILING_WHITESPACE
+	)
+	add_compile_definitions(STAMINA_BUILD_INFO="commit-${GIT_HASH}")
+elseif(STAMINA_DEBUG) 
+	add_compile_definitions(STAMINA_BUILD_INFO="debug-build")
+else()
+	add_compile_definitions(STAMINA_BUILD_INFO="release-build")
+endif()
+
+add_compile_definitions(STAMINA_VERSION_MAJOR=${STAMINA_VERSION_MAJOR})
+add_compile_definitions(STAMINA_VERSION_MINOR=${STAMINA_VERSION_MINOR})
+add_compile_definitions(STAMINA_VERSION_PATCH=${STAMINA_VERSION_PATCH})

doc/GUIInstall.md

@@ -0,0 +1,120 @@
+# How to install xSTAMINA (STAMINA GUI)
+
+I've only ever got xSTAMINA to compile on Linux, but it should properly compile on MacOS as well, and should (in theory) also run on Windows. Although Storm is not officially supported on Windows, it may be possible to attain the dependencies via KDE's `craft` package manager.
+
+## Linux
+
+This is by far the easiest way to build and try xSTAMINA.  All you will need to do is install the proper dependencies:
+
+0. Install dependencies:
+
+**Debian/Ubuntu/Derivative**
+
+```sh
+# Dependencies for Storm
+sudo apt-get -y install build-essential git cmake libboost-all-dev libcln-dev libgmp-dev libginac-dev automake libglpk-dev libhwloc-dev libz3-dev libxerces-c-dev libeigen3-dev
+# Dependencies for xSTAMINA
+sudo apt install libkf5xmlgui-dev libkf5textwidgets-dev libkf5kio-dev libkf5texteditor-dev qtbase5-dev qtdeclarative5-dev libqt5svg5-dev libkf5i18n-dev libkf5coreaddons-dev extra-cmake-modules
+```
+
+**Arch/Derivative**
+
+```sh
+# Dependencies for Storm
+sudo pacman -Syu base-devel git cmake libboost-all-dev libcln-dev libgmp-dev libginac-dev automake libglpk-dev libhwloc-dev libz3-dev libxerces-c-dev libeigen3-dev
+# Dependencies for xSTAMINA
+sudo pacman -S kde-sdk-meta
+```
+
+### Install Storm
+
+1. Clone Storm from `https://github.com/moves-rwth/storm`
+2. Invoke `cmake`
+3. Invoke `make` or `cmake --build` to build Storm (ideally with `-j <Number Threads>` flag so it doesn't take all day).
+4. Export your build path to `STORM_DIR` (`export STORM_DIR=$(pwd)`)
+
+### Install STAMINA
+
+5. Clone STAMINA from `https://github.com/fluentverification/stamina-storm`
+6. Invoke `cmake -DSTORM_PATH=$STORM_DIR -DBUILD_GUI=On`
+7. Invoke `make` or `cmake --build` to build STAMINA.
+8. This will build an executable called `xstamina`. This is the GUI.
+
+## MacOS
+
+**Note:** This assumes you have `brew`:
+
+```sh
+# Install dependencies for Storm
+brew install automake cmake boost gmp glpk hwloc z3 xerces-c
+# Install dependencies for xSTAMINA
+brew install qt@5 argp-standalone
+# Install KF5 (dependency for xSTAMINA)
+brew untap kde-mac/kde 2> /dev/null
+brew tap kde-mac/kde https://invent.kde.org/packaging/homebrew-kde.git --force-auto-update
+"$(brew --repo kde-mac/kde)/tools/do-caveats.sh"
+brew install kde-mac/kde/kf5-kwidgetsaddons kde-mac/kde/kf5-xmlgui kde-mac/kde/kf5-kio kde-mac/kde/kf5-ktexteditor
+```
+
+### Install Storm
+
+1. Clone Storm from `https://github.com/moves-rwth/storm`
+2. Invoke `cmake`
+3. Invoke `make` or `cmake --build` to build Storm (ideally with `-j <Number Threads>` flag so it doesn't take all day).
+4. Export your build path to `STORM_DIR` (`export STORM_DIR=$(pwd)`)
+
+You also may be able to install Storm directly from Brew using:
+
+```sh
+brew install stormchecker
+```
+
+Then setting `STORM_DIR` from `which storm` (it just needs to point to `libstorm.so` or `libstorm.*`.
+
+### Install STAMINA
+
+5. Clone STAMINA from `https://github.com/fluentverification/stamina-storm`
+6. Invoke `cmake -DSTORM_PATH=$STORM_DIR -DBUILD_GUI=On`
+7. Invoke `make` or `cmake --build` to build STAMINA.
+8. This will build an executable called `xstamina`. This is the GUI.
+
+## Windows
+
+**WARNING**: You are completely on your own here. I have no idea if these will even work.
+
+### Install KDE's `craft` package manager
+
+0. Install KDE's `craft` package manager: Instructions available [here](https://community.kde.org/Craft).
+
+### Install Storm
+
+**Note:** You *cannot* use MSVC/Visual Studio in order to compile Storm and therefore STAMINA/xSTAMINA as Storm will throw an error. You must install and use MinGW (and potentially cygwin).
+
+1. Install the following software for building:
+	- git
+	- cmake
+	- MinGW
+
+2. Use `craft` to install the following dependencies for Storm:
+	- boost
+	- cln
+	- gmp
+	- ginac
+	- autoreconf
+	- glpk
+	- hwloc
+	- z3
+
+(I don't know what the package names will be in `craft`, so you'll have to use `craft --search` a lot)
+
+3. Clone Storm from `https://github.com/moves-rwth/storm`
+4. Invoke `cmake` using the `-DCMAKE_CXX_COMPILER` and `-DCMAKE_C_COMPILER` variables to your MinGW compiler.
+5. Invoke `make` or `cmake --build` to build Storm (ideally with `-j <Number Threads>` flag so it doesn't take all day).
+6. Export your build path to `STORM_DIR` (`set STORM_DIR=$(pwd)`)
+
+## Install STAMINA
+
+7. Clone STAMINA from `https://github.com/fluentverification/stamina-storm`
+8. Invoke `cmake -DSTORM_PATH=$STORM_DIR -DBUILD_GUI=On`
+9. Invoke `make` or `cmake --build` to build STAMINA.
+10. This will build an executable called `xstamina`. This is the GUI.

doc/code/Core.md

@@ -0,0 +1,43 @@
+# Core of STAMINA
+
+* * *
+
+In the `stamina` namespace:
+
+## Stamina
+
+- Easy class to run STAMINA from. Used by both the CLI and GUI
+- Just tell it model and properties file, and invoke `initialize()` and `run()` (`run()` invokes `initialize()` too so you don't even need to call it yourself).
+- Get a table of results via `getResultTable()`
+
+* * *
+
+In the `stamina::core` namespace:
+
+## Options
+
+- Where all Options are defined. Static definition, so shared by the entire program
+- Must set before running
+- Can use `setArgs()` to set arguments from the arg parser used by the CLI
+
+## StaminaMessages
+
+- A number of static functions to print STAMINA-specific messages to the screen, and to the log-viewer in the GUI.
+- If compiling with the GUI, please ensure that the GUI sets the appropriate *callbacks* to put text onto its log viewer.
+- Just import `StaminaMessages.h` and then use functions.
+	+ **Info** (`StaminaMessages::info()`): general log message
+	+ **Warning** (`StaminaMessages::warning()`): warnings and stuff the user should be aware of that could negatively affect program running
+	+ **Error** (`StaminaMessages::warning()`): Noncritical error messages (if you want STAMINA to terminate please use `errorAndExit()`)
+	+ **Error and Exit** (`StaminaMessages::errorAndExit()`): critical errors that mean STAMINA must exit. Can pass in exit code as second parameter.
+- These will not print if `--quiet/-q` is included, aka if `Options::quiet` is `true`.
+
+## StateSpaceInformation
+
+- Small class used to get information about a compressed state given the current known information about the state space.
+- Must set current model's variable information (using `setVariableInformation()`) before using. This can be obtained from the model object.
+
+## StaminaModelChecker
+
+- Wrapper class which does the model checking until satisfactory for STAMINA
+- Instantiates a `StaminaModelBuilder` which it uses to build the transition matrices
+- Calls Storm to check the results.

doc/code/ModelBuilders.md

@@ -0,0 +1,37 @@
+# Model Builders
+
+All model builders must inherit from `StaminaModelBuilder` and must re-implement the following methods:
+
+```cpp
+void buildMatrices(
+	storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder
+	, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders
+	, StateAndChoiceInformationBuilder& choiceInformationBuilder
+	, boost::optional<storm::storage::BitVector>& markovianChoices
+	, boost::optional<storm::storage::sparse::StateValuationsBuilder>& stateValuationsBuilder
+);
+```
+
+and
+
+```cpp
+storm::storage::sparse::ModelComponents<ValueType, RewardModelType> buildModelComponents()
+```
+
+Generally:
+
+- `buildModelComponents()` calls `buildMatrices()`, and then builds components from the resulting sparse matrices.
+- `buildMatrices()` should be where state-space exploration occurs, and it should:
+	+ Create a callback to `StateType getOrAddStateIndex(CompressedState const& state)` which it gives to the `nextStateGenerator` instance. Inherited classes may reimplement `getOrAddStateIndex` if needed, although a base implementation is provided.
+	+ During exploration, it should *load* the current state into the next state generator, and then call `expand()` to get the successors. `nextStateGenerator` (part of `storm::generator::` and an instance of `PrismNextStateGenerator`) calls `getOrAddStateIndex`.
+	+ `getOrAddStateIndex` *should enqueue in your exploration queue!*
+- `flushToTransitionMatrix()` should be called at the end of `buildMatrices()`
+- If using the absorbing state, `setUpAbsorbingState()` should be called at the beginning of running, since the index of the absorbing state should be `0`.
+- `StaminaModelBuilder` and inherited classes are templated. They use the following template types:
+	+ `ValueType`: Generally `double`, the type in the sparse matrices
+	+ `RewardModelType`: Kept for Storm compatibility. Not used generally by STAMINA. Used for reward models
+	+ `StateType`: The type (usually a type of unsigned integer) for state indecies.
+
+Caveats:
+
+- Since `StaminaModelBuilder` is forward-declared in `BaseThread.h` the default types for `ValueType` (no default), `RewardModelType` (`storm::models::sparse::StandardRewardModel<ValueType>`), and `StateType` (`uint32_t`) are defined in that file, *not* in `StaminaModelBuilder.h`.