--------------------------------------------------------------------------------
-- Copyright © 2019 National Institute of Aerospace / Galois, Inc.
--------------------------------------------------------------------------------

-- | Fault-tolerant voting examples.

{-# LANGUAGE RebindableSyntax #-}

module Copilot.Verifier.Examples.ShouldPass.Voting where

import Language.Copilot
import Copilot.Compile.C99
import Copilot.Verifier ( Verbosity, VerifierOptions(..)
                        , defaultVerifierOptions, verifyWithOptions )

vote :: Spec
vote :: Spec
vote = do
  -- majority selects element with the biggest occurance.
  String -> Stream Bool -> [Arg] -> Spec
trigger String
"maj"  Stream Bool
true [Stream Word32 -> Arg
forall a. Typed a => Stream a -> Arg
arg Stream Word32
maj]

  -- aMajority checks if the selected element has a majority.
  String -> Stream Bool -> [Arg] -> Spec
trigger String
"aMaj" Stream Bool
true [Stream Bool -> Arg
forall a. Typed a => Stream a -> Arg
arg (Stream Bool -> Arg) -> Stream Bool -> Arg
forall a b. (a -> b) -> a -> b
$ [Stream Word32] -> Stream Word32 -> Stream Bool
forall a. (Eq a, Typed a) => [Stream a] -> Stream a -> Stream Bool
aMajority [Stream Word32]
inputs Stream Word32
maj]

  where
    maj :: Stream Word32
maj = [Stream Word32] -> Stream Word32
forall a. (Eq a, Typed a) => [Stream a] -> Stream a
majority [Stream Word32]
inputs

    -- 26 input streams to vote on
    inputs :: [Stream Word32]
    inputs :: [Stream Word32]
inputs = [ Stream Word32
a, Stream Word32
b, Stream Word32
c, Stream Word32
d, Stream Word32
e, Stream Word32
f, Stream Word32
g, Stream Word32
h, Stream Word32
i, Stream Word32
j, Stream Word32
k, Stream Word32
l, Stream Word32
m
             -- , n, o, p, q, r, s, t, u, v, w, x, y, z
             ]
    a :: Stream Word32
a = [Word32
0] [Word32] -> Stream Word32 -> Stream Word32
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Word32
a Stream Word32 -> Stream Word32 -> Stream Word32
forall a. Num a => a -> a -> a
+ Stream Word32
1
    b :: Stream Word32
b = [Word32
0] [Word32] -> Stream Word32 -> Stream Word32
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Word32
b Stream Word32 -> Stream Word32 -> Stream Word32
forall a. Num a => a -> a -> a
+ Stream Word32
1
    c :: Stream Word32
c = [Word32
0] [Word32] -> Stream Word32 -> Stream Word32
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Word32
c Stream Word32 -> Stream Word32 -> Stream Word32
forall a. Num a => a -> a -> a
+ Stream Word32
1
    d :: Stream Word32
d = [Word32
0] [Word32] -> Stream Word32 -> Stream Word32
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Word32
d Stream Word32 -> Stream Word32 -> Stream Word32
forall a. Num a => a -> a -> a
+ Stream Word32
1
    e :: Stream Word32
e = [Word32
1] [Word32] -> Stream Word32 -> Stream Word32
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Word32
e Stream Word32 -> Stream Word32 -> Stream Word32
forall a. Num a => a -> a -> a
+ Stream Word32
1
    f :: Stream Word32
f = [Word32
1] [Word32] -> Stream Word32 -> Stream Word32
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Word32
f Stream Word32 -> Stream Word32 -> Stream Word32
forall a. Num a => a -> a -> a
+ Stream Word32
1
    g :: Stream Word32
g = [Word32
1] [Word32] -> Stream Word32 -> Stream Word32
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Word32
g Stream Word32 -> Stream Word32 -> Stream Word32
forall a. Num a => a -> a -> a
+ Stream Word32
1
    h :: Stream Word32
h = [Word32
1] [Word32] -> Stream Word32 -> Stream Word32
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Word32
h Stream Word32 -> Stream Word32 -> Stream Word32
forall a. Num a => a -> a -> a
+ Stream Word32
1
    i :: Stream Word32
i = [Word32
1] [Word32] -> Stream Word32 -> Stream Word32
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Word32
i Stream Word32 -> Stream Word32 -> Stream Word32
forall a. Num a => a -> a -> a
+ Stream Word32
1
    j :: Stream Word32
j = [Word32
1] [Word32] -> Stream Word32 -> Stream Word32
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Word32
j Stream Word32 -> Stream Word32 -> Stream Word32
forall a. Num a => a -> a -> a
+ Stream Word32
1
    k :: Stream Word32
k = [Word32
1] [Word32] -> Stream Word32 -> Stream Word32
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Word32
k Stream Word32 -> Stream Word32 -> Stream Word32
forall a. Num a => a -> a -> a
+ Stream Word32
1
    l :: Stream Word32
l = [Word32
1] [Word32] -> Stream Word32 -> Stream Word32
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Word32
l Stream Word32 -> Stream Word32 -> Stream Word32
forall a. Num a => a -> a -> a
+ Stream Word32
1
    m :: Stream Word32
m = [Word32
1] [Word32] -> Stream Word32 -> Stream Word32
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Word32
m Stream Word32 -> Stream Word32 -> Stream Word32
forall a. Num a => a -> a -> a
+ Stream Word32
1
{-
    n = [1] ++ n + 1
    o = [1] ++ o + 1
    p = [1] ++ p + 1
    q = [1] ++ q + 1
    r = [1] ++ r + 1
    s = [1] ++ s + 1
    t = [1] ++ t + 1
    u = [1] ++ u + 1
    v = [1] ++ v + 1
    w = [1] ++ w + 1
    x = [1] ++ x + 1
    y = [1] ++ y + 1
    z = [1] ++ z + 1
-}

verifySpec :: Verbosity -> IO ()
--verifySpec _ = interpret 30 vote
verifySpec :: Verbosity -> IO ()
verifySpec Verbosity
verb = Spec -> IO Spec
forall a. Spec' a -> IO Spec
reify Spec
vote IO Spec -> (Spec -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= VerifierOptions -> CSettings -> [String] -> String -> Spec -> IO ()
verifyWithOptions VerifierOptions
defaultVerifierOptions{verbosity = verb}
                                                   CSettings
mkDefaultCSettings [] String
"voting"