call-alloy

A simple library to call Alloy given a specification

https://github.com/marcellussiegburg/call-alloy#readme

Version on this page:0.2.2.0
LTS Haskell 22.14:0.4.1.1
Stackage Nightly 2024-03-28:0.4.1.1
Latest on Hackage:0.4.1.1

See all snapshots call-alloy appears in

MIT licensed by Marcellus Siegburg
Maintained by [email protected]
This version can be pinned in stack with:call-alloy-0.2.2.0@sha256:af9891f33dd1fde02e4cec4b3508a42b97a8cfc8d823a8dadac2e28138fef798,3121

Module documentation for 0.2.2.0

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

  • 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 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]
  )

Changes

Changelog for call-alloy

Unreleased changes

Released changes

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. (Especially skolem may return them if variable names in predicates to check are not unique.)
  • add version constraint for Win32
  • allow later versions of bytestring