Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Theta download script #16

Merged
merged 5 commits into from
Sep 10, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 8 additions & 11 deletions plugins/xsts/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,16 +6,13 @@ Furthermore, the plugins support the automatic generation of standalone Java sta

## Setup

First, you have to set up an Eclipse with the [core Gamma plugins](https://github.com/ftsrg/gamma/tree/theta-integration/plugins/core).

Next, you have to set up [Theta](https://github.com/ftsrg/theta), more specifically the [`theta-xsts-cli` tool](https://github.com/ftsrg/theta/tree/master/subprojects/xsts-cli).
You can check out the [instructions](https://github.com/ftsrg/theta/tree/master/subprojects/xsts-cli) for various options for setting up Theta, but we suggest downloading a [binary release](https://github.com/ftsrg/theta/releases).
For Gamma, only the `theta-xsts-cli.jar` is required in addition to the libraries in the [_lib_ folder](https://github.com/ftsrg/theta/tree/master/lib).
Make sure to put the libraries onto your PATH.
Furthermore, you have to create an environment variable with the name of `THETA_XSTS_CLI_PATH`, which points to the `theta-xsts-cli.jar` binary.

Then, you have to set up the plugins in this folder:
1. Import all Eclipse projects from the the _xsts_ folder.
1. Generate the Model plugins of the `hu.bme.mit.gamma.statechart.lowlevel.model`, `hu.bme.mit.gamma.xsts.model` and `hu.bme.mit.gamma.lowlevel.xsts.transformation.traceability` using the `.genmodel` file in the respective `model` folder. The generation of additional plugins (Edit, Editor, Tests) is not necessary.
1. Set up an Eclipse with the [core Gamma plugins](https://github.com/ftsrg/gamma/tree/theta-integration/plugins/core).
1. Set up [Theta](https://github.com/ftsrg/theta), more specifically the [`theta-xsts-cli` tool](https://github.com/ftsrg/theta/tree/master/subprojects/xsts-cli) by going into the _theta-bin_ subfolder and executing `Get-Theta.ps1` (Windows) or `get-theta.sh` (Linux). The script will download the required binary and libraries.
- _Alternatively, you can check out the [instructions](https://github.com/ftsrg/theta/tree/master/subprojects/xsts-cli) for other options (e.g., build from source). For Gamma, only the `theta-xsts-cli.jar` and the Z3 libraries are required._
1. Put the downloaded libraries (dll/so files) in the _theta-bin_ folder onto your `PATH`.
1. Create an environment variable with the name of `THETA_XSTS_CLI_PATH`, which points to the downloaded `theta-xsts-cli.jar` binary.
1. Set up the plugins in this folder:
1. Import all Eclipse projects from the the _xsts_ folder.
1. Generate the Model plugins of the `hu.bme.mit.gamma.statechart.lowlevel.model`, `hu.bme.mit.gamma.xsts.model` and `hu.bme.mit.gamma.lowlevel.xsts.transformation.traceability` using the `.genmodel` file in the respective `model` folder. The generation of additional plugins (Edit, Editor, Tests) is not necessary.

Now you can use the framework in one of the following ways: you either run a runtime Eclipse and work in that or install the plugins into your host Eclipse.
40 changes: 40 additions & 0 deletions plugins/xsts/theta-bin/Get-Theta.ps1
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
$thetaVersion = "v2.4.0"
$z3release = "z3-4.5.0"
$z3version = "z3-4.5.0-x64-win"

$currentPath = (Resolve-Path .\).Path
[Net.ServicePointManager]::SecurityProtocol = [Net.SecurityProtocolType]::Tls12

function Download {
param (
$From,
$To
)
$clnt = new-object System.Net.WebClient
$clnt.DownloadFile($From, $To)
}

Write-Output "Downloading Theta binary"
Download "https://github.com/ftsrg/theta/releases/download/v2.4.0/theta-xsts-cli.jar" "$currentPath\theta-xsts-cli.jar"

Write-Output "Downloading Z3 solver binaries"
Download "https://github.com/ftsrg/theta/raw/v2.4.0/lib/libz3.dll" "$currentPath\libz3.dll"
Download "https://github.com/ftsrg/theta/raw/v2.4.0/lib/libz3java.dll" "$currentPath\libz3java.dll"

Write-Output "Downloading MSVC++ binaries"
$zipFilePath = "$currentPath\$z3version.zip"
Download "https://github.com/Z3Prover/z3/releases/download/$z3release/$z3version.zip" $zipFilePath

$shellApp = new-object -com shell.application
$zipFile = $shellApp.namespace($zipFilePath)
$dest = $shellApp.namespace($currentPath)
$dest.Copyhere($zipFile.items())

Copy-Item "$currentPath\$z3version\bin\msvcp110.dll" -Destination $currentPath
Copy-Item "$currentPath\$z3version\bin\msvcr110.dll" -Destination $currentPath
Copy-Item "$currentPath\$z3version\bin\vcomp110.dll" -Destination $currentPath

Remove-Item $zipFilePath
Remove-Item "$currentPath\$z3version" -Recurse

Write-Output "DONE"
6 changes: 6 additions & 0 deletions plugins/xsts/theta-bin/get-theta.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
#!/bin/bash
THETA_VERSION="v2.4.0"

wget "https://github.com/ftsrg/theta/releases/download/$THETA_VERSION/theta-xsts-cli.jar" -O ./theta-xsts-cli.jar
wget "https://github.com/ftsrg/theta/raw/$THETA_VERSION/lib/libz3.so" -O ./libz3.so
wget "https://github.com/ftsrg/theta/raw/$THETA_VERSION/lib/libz3java.so" -O ./libz3java.so