call-alloy: A simple library to call Alloy given a specification

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.

[maintain] [Publish]

Please see the README on GitHub at https://github.com/marcellussiegburg/call-alloy#readme


[Skip to Readme]

Properties

Versions 0.1.0.0, 0.1.0.2, 0.2.0.0, 0.2.0.1, 0.2.0.3, 0.2.0.4, 0.2.0.5, 0.2.0.6, 0.2.1.0, 0.2.1.1, 0.2.2.0, 0.2.2.0
Change log ChangeLog.md
Dependencies base (>=4.12 && <5), bytestring (>=0.10.4 && <0.12), containers (==0.6.*), directory (==1.3.*), file-embed (>=0.0.11 && <0.1), filepath (==1.4.*), hashable (>=1.2 && <1.4), mtl (==2.2.*), process (==1.6.*), split (==0.2.*), trifecta (>=2 && <2.2), unix (==2.7.*), Win32 (>=2.5 && <2.14) [details]
License MIT
Copyright 2019-2020 Marcellus Siegburg
Author Marcellus Siegburg
Maintainer marcellus.siegburg@uni-due.de
Category Language
Home page https://github.com/marcellussiegburg/call-alloy#readme
Bug tracker https://github.com/marcellussiegburg/call-alloy/issues
Source repo head: git clone https://github.com/marcellussiegburg/call-alloy
Uploaded by marcellus at 2021-09-17T17:12:21Z

Modules

[Index]

Downloads

Maintainer's Corner

For package maintainers and hackage trustees


Readme for call-alloy-0.2.2.0

[back to package description]

call-alloy Build Status

This is a simple library to call Alloy given a specification. This package includes a simple Java Library to make an API call to the Alloy Library. Alloy is included (as JAR file) within this library as well.

Requriements

Please note

The Java interface to get Alloy instances as well as the Alloy Jar file are backed into this library.

On every call the application checks the XdgDirectory if the libraries exist in a current version. If not they are placed there together with a version identifier.

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:

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 Nodes, which might have some goods stored and may deliver them to other Nodes (via flow). Nodes 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 Nodes 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 (abbreviated) instance:

[(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 = 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 = 0},Object {objSig = "Node", identifier = 1},NumberObject {number = 0}),
        (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:

newtype Node = Node Int deriving (Eq, Show, Ord)

instanceToNames
  :: AlloyInstance
  -> Either String (Set Node, Set (Node, Int), Set (Node, Node, Int), Set (Node), Set (Node))
instanceToNames insta = do
  let node :: String -> Int -> Either String 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:

Right (
  fromList [Node 0,Node 1],
  fromList [(Node 0,0),(Node 1,1)],
  fromList [(Node 0,Node 1,0),(Node 1,Node 0,3)],
  fromList [Node 1],
  fromList [Node 0]
  )