diff options
| author | Camil Staps | 2018-07-05 14:55:11 +0200 |
|---|---|---|
| committer | Camil Staps | 2018-07-05 14:55:11 +0200 |
| commit | 546147b611a30f508e09ae0180487a11426a233f (patch) | |
| tree | b61b99a257eb7a6286df318da7e63ea5d4689e43 /Assignment2/src/Z3.dcl | |
| parent | New DTMC structure (diff) | |
| parent | Merge branch 'master' of gitlab.science.ru.nl:eveen/Model-Checking (diff) | |
Merge branch 'master' of gitlab.science.ru.nl:eveen/Model-Checking
Diffstat (limited to 'Assignment2/src/Z3.dcl')
| -rw-r--r-- | Assignment2/src/Z3.dcl | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/Assignment2/src/Z3.dcl b/Assignment2/src/Z3.dcl new file mode 100644 index 0000000..0329987 --- /dev/null +++ b/Assignment2/src/Z3.dcl @@ -0,0 +1,13 @@ +definition module Z3 + +from System.Process import :: ProcessHandle, :: ProcessIO + +:: Z3 + +startZ3 :: *World -> (Z3, *World) +addAssert :: Z3 String *World -> *World +addVariable :: Z3 String *World -> *World +checkSat :: Z3 *World -> (Bool, *World) + +// Note: getModel terminates z3 +getModel :: Z3 *World -> (String, *World) |