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.3, 0.3.0.1, 0.3.0.2, 0.3.0.3, 0.4, 0.4.0.1, 0.4.0.2, 0.4.0.3, 0.4.1, 0.4.1.1, 0.5, 0.5.0.1, 0.5.0.1
Change log ChangeLog.md
Dependencies async (>=2.2.1 && <2.3), base (>=4.12 && <5), bytestring (>=0.10.4 && <0.13), containers (>=0.6 && <0.8), directory (>=1.3 && <1.4), exceptions (>=0.8.1 && <0.11), extra (>=1.7 && <1.8), filepath (>=1.4 && <1.5), process (>=1.6 && <1.7), split (>=0.2 && <0.3), transformers (>=0.5.0.0 && <0.7), trifecta (>=2 && <2.2), unix (>=2.7 && <2.9), Win32 (>=2.5 && <2.15) [details]
License MIT
Copyright 2019-2024 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 2024-04-24T10:38:14Z

Modules

[Index] [Quick Jump]

Flags

Manual Flags

NameDescriptionDefault
test-different-solvers

During tests different solvers are called to test if they are working on the current system

Disabled

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees


Readme for call-alloy-0.5.0.1

[back to package description]

call-alloy Haskell CI

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

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