This is a fork of the Heterogeneous Toolset (Hets), extending it with support for simple UML State Machines and Composite Structures. The implementation forms part of my PhD thesis project. We intend to integrate it into upstream Hets, but this version is meant to reflect the software as it was used in the thesis.
For more information on upstream Hets, please consult the project home page or the github project.
The main work done on Hets in this thesis is contained in the following files:
.
├── UMLState
│ └── Logic_UMLState.hs UMLState: a language for State Machines without output events
├── UMLStateO
│ └── Logic_UMLStateO.hs UMLStateO: a language for State Machines without output events
├── UMLComp
│ └── Logic_UMLComp.hs UMLComp: a language for Composite Structures
│ and translation to CASL (works with UMLStateO)
├── Comorphisms
│ ├── UMLState2CASL.hs translation from UMLState to CASL
│ └── UMLStateO2CASL.hs translation from UMLStateO to CASL
├── build.sh support for building with the same dependency versions I use
├── nix support for building with the same dependency versions I use
│ └── ...
└── test support for building with the same dependency versions I use
└── UMLTests
└── atmmod.het an example input file for UMLState and UMLComp
UMLState is included because it has been used for a verification example in the thesis.
It is the direct predecessor, both in terms of theory and code, of UMLStateO.
We would probably only merge UMLStateO into upstream and consider it to supersede UMLState -- however, this will be decided in discussion with the Hets team.
I had to use some specific, older versions of dependencies to get this to build.
It is possible to build with the same dependency versions I used through the Nix package manager.
For this to work, it is necessary to first install Nix.
Then, build.sh can be used as a wrapper around the Makefile.
This has been tested on the platforms x86_64-darwin (MacOS) and x86_64-linux (specifically: NixOS). Linux distributions other than Linux should work as well.
For other systems, or other CPU architectures, it would at least be necessary to add a download of the uDrawGraph dependency in ./nix/uDrawGraph.nix.
A caveat on reproducibility: The downloads of the Hets-lib sources report conflicting hashes for nominally identical versions. Therefore, the hash checks for Hets-lib have been deactivated. Hets itself should build even without Hets-lib.
./build.sh stack
will download both Haskell and system dependencies.
After running this once, as long as dependencies don't change, Hets can always be built and rebuilt using:
./build.sh
A shell with the dependencies available can be started using:
nix-shell nix/hets.nix
An interactive Haskell session configured for the Hets project is available through:
./build.sh ghci