call-alloy
A simple library to call Alloy given a specification
https://github.com/marcellussiegburg/call-alloy#readme
LTS Haskell 22.42: | 0.4.1.1 |
Stackage Nightly 2024-11-19: | 0.5.0.1@rev:2 |
Latest on Hackage: | 0.5.0.1@rev:2 |
call-alloy-0.5.0.1@sha256:7563481b6a8441d3d03c4cb492b3a73c73f2f96fa00cf273f12092a85433fe41,3927
Module documentation for 0.5.0.1
- Language
- Language.Alloy
call-alloy
This is a simple library to call Alloy given a specification. This package installs a simple Java Library to make an API call to the Alloy Library. Alloy is installed (as JAR file) alongside this library as well.
Requirements
- Java Runtime Environment: There is currently no warning if you have not set up any Java Runtime Environment. However, you will get runtime errors if it is not available when a call to Alloy happens. If you want to force a check, perform the test cases.
Please note
The Java interface to get Alloy instances as well as the Alloy Jar file are installed together with this library using usual cabal means (data directory).
The library in action
This is a basic description on how to use the library.
A specification example
Consider this Alloy specification of a simple Graph:
# test/unit/readmeExampleSpecification.als
abstract sig Node {
flow : Node -> lone Int,
stored : one Int
} {
stored >= 0
all n : Node | some flow[n] implies flow[n] >= 0
no flow[this]
}
fun currentFlow(x, y : one Node) : Int {
let s = x.stored, f = x.flow[y] | s < f implies s else f
}
pred withFlow[x, y : one Node] {
currentFlow[x, y] > 0
}
pred show {}
run withFlow for 3 Int, 2 Node
The graph is consisting of Node
s, which might have some goods stored
and may deliver them to other Node
s (via flow
).
Node
s do not have flow
to themselves.
The currentFlow
is the minimum between the flow from the starting Node
to the end Node
and the currently stored
goods at the starting Node
(note: intermediate Node
s are not allowed).
We call two Nodes
x
and y
withFlow
if currentFlow
from x
to y
is greater than 0
.
We restrict our search to 3
-Bit signed Int
values and 2
Nodes
.
An instance example
Calling Alloy using getInstances
and the above program
could return the following instance:
-- test/unit/readmeExampleInstance.hs
fromList [
( Signature {scope = Nothing, sigName = "$withFlow_x"},
Entry {
annotation = Just Skolem,
relation = fromList [
( "",
Single (fromList [
Object {objSig = "Node", identifier = 1}
]))
]
}),
( Signature {scope = Nothing, sigName = "$withFlow_y"},
Entry {
annotation = Just Skolem,
relation = fromList [
( "",
Single (fromList [
Object {objSig = "Node", identifier = 0}
]))
]
}),
( Signature {scope = Nothing, sigName = "Int"},
Entry {
annotation = Nothing,
relation = fromList [
( "",
Single (fromList [
NumberObject {number = -4},
NumberObject {number = -3},
NumberObject {number = -2},
NumberObject {number = -1},
NumberObject {number = 0},
NumberObject {number = 1},
NumberObject {number = 2},
NumberObject {number = 3}
]))
]
}),
( Signature {scope = Nothing, sigName = "String"},
Entry {
annotation = Nothing,
relation = fromList [("", EmptyRelation)]
}),
( Signature {scope = Nothing, sigName = "end"},
Entry {
annotation = Nothing,
relation = fromList [
( "",
Id (NumberObject {number = 0}))
]
}),
( Signature {scope = Nothing, sigName = "integers"},
Entry {
annotation = Nothing,
relation = fromList [
( "",
Single (fromList [
NumberObject {number = -4},
NumberObject {number = -3},
NumberObject {number = -2},
NumberObject {number = -1},
NumberObject {number = 0},
NumberObject {number = 1},
NumberObject {number = 2},
NumberObject {number = 3}
]))
]
}),
( Signature {scope = Nothing, sigName = "loop"},
Entry {
annotation = Nothing,
relation = fromList [
( "",
Id (NumberObject {number = 0}))
]
}),
( Signature {scope = Nothing, sigName = "none"},
Entry {
annotation = Nothing,
relation = fromList [("", EmptyRelation)]
}),
( Signature {scope = Nothing, sigName = "univ"},
Entry {
annotation = Nothing,
relation = fromList [
( "",
Single (fromList [
Object {objSig = "Node", identifier = 0},
Object {objSig = "Node", identifier = 1},
NumberObject {number = -4},
NumberObject {number = -3},
NumberObject {number = -2},
NumberObject {number = -1},
NumberObject {number = 0},
NumberObject {number = 1},
NumberObject {number = 2},
NumberObject {number = 3}
]))
]
}),
( Signature {scope = Just "seq", sigName = "Int"},
Entry {
annotation = Nothing,
relation = fromList [
( "",
Single (fromList [
NumberObject {number = 0},
NumberObject {number = 1},
NumberObject {number = 2}
]))
]
}),
( Signature {scope = Just "this", sigName = "Node"},
Entry {
annotation = Nothing,
relation = fromList [
( "",
Single (fromList [
Object {objSig = "Node", identifier = 0},
Object {objSig = "Node", identifier = 1}
])),
( "flow",
Triple (fromList [
( Object {objSig = "Node", identifier = 1},
Object {objSig = "Node", identifier = 0},
NumberObject {number = 3})
])),
( "stored",
Double (fromList [
( Object {objSig = "Node", identifier = 0},
NumberObject {number = 0}),
( Object {objSig = "Node", identifier = 1},
NumberObject {number = 1})
]))
]
})
]
A retrieval example
Using this library we may retrieve returned signature values using lookupSig
,
then query parameter variables of the queried predicate using unscoped
,
and query signature sets and relations using getSingleAs
, getDoubleAs
, and getTripleAs
.
The following Code might for instance be used for the graph example:
-- test/readmeExample.hs
module ReadmeExample (
Node (Node),
instanceToNames,
) where
import Control.Monad.Catch (MonadThrow)
import Data.Set (Set)
import Language.Alloy.Call (
AlloyInstance,
getDoubleAs,
getSingleAs,
getTripleAs,
int,
lookupSig,
object,
scoped,
unscoped,
)
newtype Node = Node Int deriving (Eq, Show, Ord, Read)
instanceToNames
:: MonadThrow m
=> AlloyInstance
-> m (Set Node, Set (Node, Int), Set (Node, Node, Int), Set Node, Set Node)
instanceToNames insta = do
let node :: MonadThrow m => String -> Int -> m Node
node = object "Node" Node
n <- lookupSig (scoped "this" "Node") insta
nodes <- getSingleAs "" node n
store <- getDoubleAs "stored" node int n
flow <- getTripleAs "flow" node node int n
x <- lookupSig (unscoped "$withFlow_x") insta >>= getSingleAs "" node
y <- lookupSig (unscoped "$withFlow_y") insta >>= getSingleAs "" node
return (nodes, store, flow, x, y)
Calling instanceToNames
on the above instance would result in the following expression:
-- test/unit/readmeExampleResult.hs
(
fromList [Node 0,Node 1],
fromList [(Node 0,0),(Node 1,1)],
fromList [(Node 1,Node 0,3)],
fromList [Node 1],
fromList [Node 0]
)
Changes
Changelog for call-alloy
Unreleased changes
Released changes
0.5
- use MonadThrow instead of MonadError
- add Readme eample to test cases
0.4.1.1
- introduce flag for testing different SAT solvers
0.4.1
- add support for different SAT solvers
0.4.0.3
- fix terminal spamming due to process abortion on Windows
0.4.0.2
- make resilient to IO errors due to parallelism or abort
0.4.0.1
- fix too early abortion of process execution
- show raw output on library parsing issues
0.4
- provide required Java libraries in package data directory
- use async for process interaction
- terminate calls to Java properly (even on interrupts)
0.3.0.3
- fix runtime error on WARN
0.3.0.2
- fix runtime error on PARTIAL_INSTANCE
0.3.0.1
- support “State0” line in retrieved instances (introduced by Alloy 6)
- support CRLF at line end
0.3
- upgrade to Alloy 6.0.0
- allow slashes in object names
- allow identity relations
- improve feedback on misspelled/missing relation and signature names
- remove ‘relToMap’
0.2.2.0
- deprecate ‘relToMap’
- provide functions for returning raw output of instances
- provide functions for typed retrieval
- deprecate ‘getSingle’, ‘getDouble’, ‘getTriple’, ‘objectName’
0.2.1.1
- fix errors due to long Alloy code by starting timeout after transferring code
0.2.1.0
- enable to abort instance generation early by using timeout
0.2.0.6
- allow parsing
'
as part of words. (Especiallyskolem
may return them if variable names in predicates to check are not unique.) - add version constraint for
Win32
- allow later versions of
bytestring