Commit da47ada7 authored by dterei's avatar dterei

Remove fibon files

parent a9cdc8b1
{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
module Fibon.Benchmarks.Hackage.Agum.Fibon.Instance(
mkInstance
)
where
import Fibon.BenchmarkInstance
sharedConfig = BenchmarkInstance {
flagConfig = FlagConfig {
configureFlags = []
, buildFlags = []
, runFlags = []
}
, stdinInput = Just "eqn.txt"
, output = [(Stdout, Diff "agum.stdout.expected")]
, exeName = "agum"
}
flgCfg = flagConfig sharedConfig
mkInstance Test = sharedConfig {
flagConfig = flgCfg
}
mkInstance Ref = sharedConfig {
flagConfig = flgCfg
}
The gen.hs program can be used to generate inputs. The eqn.txt for the
ref input was generated by
$ ./gen 1 2
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
Abelian group unification and matching -- :? for help
agum> Problem: 2x + y = 3z
Unifier: [x : g0,y : -2g0 + 3g2,z : g2]
Matcher: [x : g0,y : -2g0 + 3z]
agum>
module Main where
import Data.List ( sortBy )
import Data.Ord ( comparing )
import System.Random
import Control.Monad.State
import System.Environment
vars = ('a', 'z')
maxVars = 1000
maxMult = 9999 :: Int
main :: IO ()
main = do
[s,n] <- getArgs -- Seed,NumberOfEquations
let gen = mkStdGen (read s)
es = evalState (eqns (read n)) gen
putStr $ unlines es
eqns :: Int -> EqnState [String]
eqns cnt = sequence (replicate cnt eqn)
eqn :: EqnState String
eqn = do
lhs <- formula
rhs <- formula
return $ lhs ++ "=" ++ rhs
formula :: EqnState String
formula = do
g <- get
let (n, g') = randomR (1, maxVars) g
put g'
vs <- sequence $ replicate n factor
fs <- sequence $ replicate (n-1) function
return $ concat (interleave vs fs)
type EqnState a = State (StdGen) a
factor :: EqnState String
factor = do
g <- get
let (v, g') = randomR (1, maxVars) g --randomR vars g
(m, g'') = randomR (1, maxMult) g'
put g''
return $ (show m) ++ "x" ++ show v
function :: EqnState String
function = do
g <- get
let (b, g') = randomR (True, False) g
put g'
return $ if b then "+" else "-"
interleave :: [a] -> [a] -> [a]
interleave [] _ = []
interleave [x] _ = [x]
interleave xs [] = xs
interleave (x:xs) (y:ys) = [x,y] ++ interleave xs ys
import Distribution.Simple
main = defaultMain
Name: agum
Version: 2.3
Maintainer: ramsdell@mitre.org
Cabal-Version: >= 1.2
License: GPL
License-File: license.txt
Synopsis: Unification and Matching in an Abelian Group
Description: The unification problem is given the problem
statement t =? t\', find a most general
substitution s such that s(t) = s(t\') modulo
the axioms of an Abelian group. The matching
problem is to find a most general substitution
s such that s(t) = t\' modulo the axioms.
Substitition s is more general than s\' if
there is a substitition s\" such that s\' =
s\" o s.
Category: Algebra
Build-Type: Simple
Extra-Source-Files: readme.txt ChangeLog Makefile
Library
Buildable: False
Build-Depends: base >= 3 && < 5, containers
Exposed-Modules: Algebra.AbelianGroup.UnificationMatching
Algebra.AbelianGroup.IntLinEq
Hs-Source-Dirs: src
GHC-Options:
-Wall -fno-warn-name-shadowing -fwarn-unused-imports
Executable agum
Main-Is: Algebra/AbelianGroup/Main.hs
Build-Depends: base >= 3 && < 5, containers
Other-Modules: Algebra.AbelianGroup.UnificationMatching
Algebra.AbelianGroup.IntLinEq
Hs-Source-Dirs: src
GHC-Options:
-Wall -fno-warn-name-shadowing -fwarn-unused-imports
{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
module Fibon.Benchmarks.Hackage.Bzlib.Fibon.Instance(
mkInstance
)
where
import Fibon.BenchmarkInstance
sharedConfig = BenchmarkInstance {
flagConfig = FlagConfig {
configureFlags = []
, buildFlags = []
, runFlags = []
}
, stdinInput = Nothing
, output = []
, exeName = "hsbzip"
}
flgCfg = flagConfig sharedConfig
mkInstance Test = sharedConfig {
flagConfig = flgCfg {
runFlags = ["bzlib.cabal.bz2"]
}
, output = [(OutputFile "bzlib.cabal.bz2.roundtrip",
Diff "bzlib.cabal.bz2")]
}
mkInstance Ref = sharedConfig {
flagConfig = flgCfg {
runFlags = ["mito.aa.bz2"]
}
, output = [(OutputFile "mito.aa.bz2.roundtrip",
Diff "mito.aa.bz2")]
}
import Distribution.Simple
main = defaultMain
name: bzlib
version: 0.5.0.0
copyright: (c) 2006-2008 Duncan Coutts
license: BSD3
license-file: LICENSE
author: Duncan Coutts <duncan@haskell.org>
maintainer: Duncan Coutts <duncan@haskell.org>
category: Codec
synopsis: Compression and decompression in the bzip2 format
description: This package provides a pure interface for compressing and
decompressing streams of data represented as lazy
'ByteString's. It uses the bz2 C library so it has high
performance.
.
It provides a convenient high level api suitable for most
tasks and for the few cases where more control is needed it
provides access to the full bzip2 feature set.
stability: provisional
build-type: Simple
cabal-version: >= 1.2.1
extra-source-files: cbits/bzlib_private.h
-- demo programs:
bzip2.hs bunzip2.hs
flag bytestring-in-base
description: In the ghc-6.6 era the bytestring modules were
included in the base package.
library
buildable: False
exposed-modules: Codec.Compression.BZip,
Codec.Compression.BZip.Internal
other-modules: Codec.Compression.BZip.Stream
extensions: CPP, ForeignFunctionInterface
if flag(bytestring-in-base)
-- bytestring was in base-2.0 and 2.1.1
build-depends: base >= 2.0 && < 2.2
cpp-options: -DBYTESTRING_IN_BASE
else
build-depends: base < 2.0 || >= 2.2, bytestring >= 0.9
includes: bzlib.h
ghc-options: -Wall
if !os(windows)
-- Normally we use the the standard system bz2 lib:
extra-libraries: bz2
else
-- However for the benefit of users of Windows (which does not have zlib
-- by default) we bundle a complete copy of the C sources of bzip2-1.0.5
c-sources: cbits/blocksort.c cbits/bzlib.c cbits/compress.c
cbits/crctable.c cbits/decompress.c cbits/huffman.c
cbits/randtable.c
include-dirs: cbits
install-includes: bzlib.h
executable hsbzip
main-is: Main.hs
other-modules: Codec.Compression.BZip.Stream
build-depends: base > 3 && < 5, bytestring >= 0.9
includes: bzlib.h
c-sources: cbits/blocksort.c cbits/bzlib.c cbits/compress.c
cbits/crctable.c cbits/decompress.c cbits/huffman.c
cbits/randtable.c
include-dirs: cbits
{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
module Fibon.Benchmarks.Hackage.Cpsa.Fibon.Instance(
mkInstance
)
where
import Fibon.BenchmarkInstance
sharedConfig = BenchmarkInstance {
flagConfig = FlagConfig {
configureFlags = []
, buildFlags = []
, runFlags = []
}
, stdinInput = Nothing
, output = [(Stdout, Diff "cpsa.stdout.expected")]
, exeName = "cpsa"
}
flgCfg = flagConfig sharedConfig
mkInstance Test = sharedConfig {
flagConfig = flgCfg {runFlags = ["ns.scm"]}
}
mkInstance Ref = sharedConfig {
flagConfig = flgCfg {runFlags = ["nsl5.lisp"]}
}
(defprotocol nsl5 basic
(defrole init
(vars (a b c d e name)
(na0 na1 na2 na3 nb0 nb1 nb2 nb3 nc0 nc1 nc2 nc3 nd0 nd1 nd2 nd3
ne0 ne1 ne2 ne3 text))
(trace
(send
(enc na0 a c d e (enc na1 a b d e (pubk c))
(enc na2 a b c e (pubk d)) (enc na3 a b c d (pubk e))
(pubk b)))
(recv
(enc na3 ne0 e b c d (enc na0 nb3 b c d e (pubk a))
(enc na1 nc2 c b d e (pubk a)) (enc na2 nd1 d e b c (pubk a))
(enc nb0 nc3 c d e a (pubk b)) (enc nb1 nd2 d c e a (pubk b))
(enc nb2 ne1 e a c d (pubk b)) (enc nc0 nd3 d e a b (pubk c))
(enc nc1 ne2 e a b d (pubk c)) (enc nd0 ne3 e a b c (pubk d))
(pubk a)))
(send
(enc nb3 (enc nb0 nc3 c d e a (pubk b))
(enc nb1 nd2 d c e a (pubk b)) (enc nb2 ne1 e a c d (pubk b))
(enc nc0 nd3 d e a b (pubk c)) (enc nc1 ne2 e a b d (pubk c))
(enc nc2 (pubk c)) (enc nd0 ne3 e a b c (pubk d))
(enc nd1 (pubk d)) (enc ne0 (pubk e)) (pubk b))))
(uniq-orig na0 na1 na2 na3))
(defrole resp1
(vars (a b c d e name)
(na0 na1 na2 na3 nb0 nb1 nb2 nb3 nc0 nc1 nc2 nc3 nd0 nd1 nd2 nd3
ne0 ne1 ne2 ne3 text))
(trace
(recv
(enc na0 a c d e (enc na1 a b d e (pubk c))
(enc na2 a b c e (pubk d)) (enc na3 a b c d (pubk e))
(pubk b)))
(send
(enc nb0 b d e a (enc na1 a b d e (pubk c))
(enc na2 a b c e (pubk d)) (enc nb1 b c e a (pubk d))
(enc na3 a b c d (pubk e)) (enc nb2 b c d a (pubk e))
(enc na0 nb3 b c d e (pubk a)) (pubk c)))
(recv
(enc nb3 (enc nb0 nc3 c d e a (pubk b))
(enc nb1 nd2 d c e a (pubk b)) (enc nb2 ne1 e a c d (pubk b))
(enc nc0 nd3 d e a b (pubk c)) (enc nc1 ne2 e a b d (pubk c))
(enc nc2 (pubk c)) (enc nd0 ne3 e a b c (pubk d))
(enc nd1 (pubk d)) (enc ne0 (pubk e)) (pubk b)))
(send
(enc nc3 (enc nc0 nd3 d e a b (pubk c))
(enc nc1 ne2 e a b d (pubk c)) (enc nc2 (pubk c))
(enc nd0 ne3 e a b c (pubk d)) (enc nd1 (pubk d))
(enc nd2 (pubk d)) (enc ne0 (pubk e)) (enc ne1 (pubk e))
(pubk c))))
(uniq-orig nb0 nb1 nb2 nb3))
(defrole resp2
(vars (a b c d e name)
(na0 na1 na2 na3 nb0 nb1 nb2 nb3 nc0 nc1 nc2 nc3 nd0 nd1 nd2 nd3
ne0 ne1 ne2 ne3 text))
(trace
(recv
(enc nb0 b d e a (enc na1 a b d e (pubk c))
(enc na2 a b c e (pubk d)) (enc nb1 b c e a (pubk d))
(enc na3 a b c d (pubk e)) (enc nb2 b c d a (pubk e))
(enc na0 nb3 b c d e (pubk a)) (pubk c)))
(send
(enc nc0 c e a b (enc na2 a b c e (pubk d))
(enc nb1 b c e a (pubk d)) (enc na3 a b c d (pubk e))
(enc nb2 b c d a (pubk e)) (enc nc1 c d a b (pubk e))
(enc na0 nb3 b c d e (pubk a)) (enc na1 nc2 c b d e (pubk a))
(enc nb0 nc3 c d e a (pubk b)) (pubk d)))
(recv
(enc nc3 (enc nc0 nd3 d e a b (pubk c))
(enc nc1 ne2 e a b d (pubk c)) (enc nc2 (pubk c))
(enc nd0 ne3 e a b c (pubk d)) (enc nd1 (pubk d))
(enc nd2 (pubk d)) (enc ne0 (pubk e)) (enc ne1 (pubk e))
(pubk c)))
(send
(enc nd3 (enc nd0 ne3 e a b c (pubk d)) (enc nd1 (pubk d))
(enc nd2 (pubk d)) (enc ne0 (pubk e)) (enc ne1 (pubk e))
(enc ne2 (pubk e)) (pubk d))))
(uniq-orig nc0 nc1 nc2 nc3))
(defrole resp3
(vars (a b c d e name)
(na0 na1 na2 na3 nb0 nb1 nb2 nb3 nc0 nc1 nc2 nc3 nd0 nd1 nd2 nd3
ne0 ne1 ne2 ne3 text))
(trace
(recv
(enc nc0 c e a b (enc na2 a b c e (pubk d))
(enc nb1 b c e a (pubk d)) (enc na3 a b c d (pubk e))
(enc nb2 b c d a (pubk e)) (enc nc1 c d a b (pubk e))
(enc na0 nb3 b c d e (pubk a)) (enc na1 nc2 c b d e (pubk a))
(enc nb0 nc3 c d e a (pubk b)) (pubk d)))
(send
(enc nd0 d a b c (enc na3 a b c d (pubk e))
(enc nb2 b c d a (pubk e)) (enc nc1 c d a b (pubk e))
(enc na0 nb3 b c d e (pubk a)) (enc na1 nc2 c b d e (pubk a))
(enc na2 nd1 d e b c (pubk a)) (enc nb0 nc3 c d e a (pubk b))
(enc nb1 nd2 d c e a (pubk b)) (enc nc0 nd3 d e a b (pubk c))
(pubk e)))
(recv
(enc nd3 (enc nd0 ne3 e a b c (pubk d)) (enc nd1 (pubk d))
(enc nd2 (pubk d)) (enc ne0 (pubk e)) (enc ne1 (pubk e))
(enc ne2 (pubk e)) (pubk d)))
(send
(enc ne3 (enc ne0 (pubk e)) (enc ne1 (pubk e))
(enc ne2 (pubk e)) (pubk e))))
(uniq-orig nd0 nd1 nd2 nd3))
(defrole resp4
(vars (a b c d e name)
(na0 na1 na2 na3 nb0 nb1 nb2 nb3 nc0 nc1 nc2 nc3 nd0 nd1 nd2 nd3
ne0 ne1 ne2 ne3 text))
(trace
(recv
(enc nd0 d a b c (enc na3 a b c d (pubk e))
(enc nb2 b c d a (pubk e)) (enc nc1 c d a b (pubk e))
(enc na0 nb3 b c d e (pubk a)) (enc na1 nc2 c b d e (pubk a))
(enc na2 nd1 d e b c (pubk a)) (enc nb0 nc3 c d e a (pubk b))
(enc nb1 nd2 d c e a (pubk b)) (enc nc0 nd3 d e a b (pubk c))
(pubk e)))
(send
(enc na3 ne0 e b c d (enc na0 nb3 b c d e (pubk a))
(enc na1 nc2 c b d e (pubk a)) (enc na2 nd1 d e b c (pubk a))
(enc nb0 nc3 c d e a (pubk b)) (enc nb1 nd2 d c e a (pubk b))
(enc nb2 ne1 e a c d (pubk b)) (enc nc0 nd3 d e a b (pubk c))
(enc nc1 ne2 e a b d (pubk c)) (enc nd0 ne3 e a b c (pubk d))
(pubk a)))
(recv
(enc ne3 (enc ne0 (pubk e)) (enc ne1 (pubk e))
(enc ne2 (pubk e)) (pubk e))))
(uniq-orig ne0 ne1 ne2 ne3)))
(defskeleton nsl5 (vars (a b c d e name))
(defstrand init 3 (a a) (b b) (c c) (d d) (e e))
(non-orig (privk a) (privk b) (privk c) (privk d) (privk e)))
(defskeleton nsl5 (vars (a b c d e name))
(defstrand resp1 4 (a a) (b b) (c c) (d d) (e e))
(non-orig (privk a) (privk b) (privk c) (privk d) (privk e)))
(defskeleton nsl5 (vars (a b c d e name))
(defstrand resp2 4 (a a) (b b) (c c) (d d) (e e))
(non-orig (privk a) (privk b) (privk c) (privk d) (privk e)))
(defskeleton nsl5 (vars (a b c d e name))
(defstrand resp3 4 (a a) (b b) (c c) (d d) (e e))
(non-orig (privk a) (privk b) (privk c) (privk d) (privk e)))
(defskeleton nsl5 (vars (a b c d e name))
(defstrand resp4 3 (a a) (b b) (c c) (d d) (e e))
(non-orig (privk a) (privk b) (privk c) (privk d) (privk e)))
This source diff could not be displayed because it is too large. You can view the blob instead.
;;; Needham-Schroeder Protocol
(defprotocol ns basic
(defrole init
(vars (a b name) (n1 n2 text))
(trace
(send (enc n1 a (pubk b)))
(recv (enc n1 n2 (pubk a)))
(send (enc n2 (pubk b)))))
(defrole resp
(vars (b a name) (n2 n1 text))
(trace
(recv (enc n1 a (pubk b)))
(send (enc n1 n2 (pubk a)))
(recv (enc n2 (pubk b)))))
(comment "Needham-Schroeder with no role origination assumptions"))
;;; The initiator point-of-view
(defskeleton ns
(vars (a b name) (n1 text))
(defstrand init 3 (a a) (b b) (n1 n1))
(non-orig (privk b) (privk a))
(uniq-orig n1)
(comment "Initiator point-of-view"))
;;; The responder point-of-view
(defskeleton ns
(vars (a name) (n2 text))
(defstrand resp 3 (a a) (n2 n2))
(non-orig (privk a))
(uniq-orig n2)
(comment "Responder point-of-view"))
;;; Needham-Schroeder Protocol with origination assumptions on roles
;;; This
(defprotocol ns-role-origs basic
(defrole init
(vars (a b name) (n1 n2 text))
(trace
(send (enc n1 a (pubk b)))
(recv (enc n1 n2 (pubk a)))
(send (enc n2 (pubk b))))
(non-orig (privk b))
(uniq-orig n1))
(defrole resp
(vars (b a name) (n2 n1 text))
(trace
(recv (enc n1 a (pubk b)))
(send (enc n1 n2 (pubk a)))
(recv (enc n2 (pubk b))))
(non-orig (privk a))
(uniq-orig n2))
(comment "Needham-Schroeder with role assumptions that are too strong"))
;;; The initiator point-of-view
(defskeleton ns-role-origs
(vars)
(defstrand init 3))
;;; The responder point-of-view
(defskeleton ns-role-origs
(vars)
(defstrand resp 3))
;;; Needham-Schroeder Protocol with a doubled nonce. Look at the
;;; first message in each role.
(defprotocol ns2 basic
(defrole init
(vars (a b name) (n1 n2 n3 text))
(trace
(send (enc n1 n3 a (pubk b)))
(recv (enc n1 n2 (pubk a)))
(send (enc n2 (pubk b)))))
(defrole resp
(vars (b a name) (n2 n1 text))
(trace
(recv (enc n1 n1 a (pubk b)))
(send (enc n1 n2 (pubk a)))
(recv (enc n2 (pubk b))))
(note doubled nonce in the first message))
(note that this protocol is derived from Needham-Schroeder))
(defskeleton ns2
(vars (a b name) (n1 text))
(defstrand init 3 (a a) (b b) (n1 n1))
(non-orig (privk b) (privk a))
(uniq-orig n1)
(note the disappearance of this note))
;;; Note that the association list style key-value pairs that follow
;;; the list of strands can be supplied in any order, and values with
;;; the same key are appended together. Check the output to see how
;;; CPSA interprets this input.
(defskeleton ns
(vars (n1 n2 text) (a b name))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))
(non-orig (privk b))
(precedes ((0 0) (1 0)))
(non-orig (privk a))
(uniq-orig n1)
(precedes ((1 1) (0 1))))
import Distribution.Simple
main = defaultMain
Name: cpsa
Version: 2.1.0
Maintainer: ramsdell@mitre.org
Cabal-Version: >= 1.6
License: BSD3