robstewart57

Prelude> data D = D Int
Prelude> let f (D i) = "ok"
Prelude> f undefined
"*** Exception: Prelude.undefined
Prelude> newtype D = D Int
Prelude> let f (D i) = "ok"
Prelude> f undefined
"ok"

robstewart57

{-# LANGUAGE DeriveDataTypeable #-}

import Control.Concurrent (threadDelay)
import Control.Exception (Exception,throw)
import Control.Monad (void)
import Control.Concurrent.Async (Async,race,wait,withAsync)
import Data.Typeable (Typeable)

data ThreadTimeoutException = ThreadTimeoutException
     deriving (Show, Typeable)

robstewart57

mtype = { FISH , RESCHEDULE , SCHEDULE , SCHEDULEREQ , SCHEDULEAUTH , ACK , NOWORK , SENDFAILED , PING } ; // message payload types
mtype = { ONNODE , INTRANSITION }; // spark.status types

typedef Node {
  chan inChan = [50] of {mtype, chan } ;
  bool hasSpark;
  bool waitingFish;
  bool waitingSchedAuth;
  bool dead;
};

robstewart57

mtype = { PING , PONG , INFO } ;

typedef Node {
  chan inChan = [50] of {mtype } ;
  bool receivedInfo;
};
Node nodes[2];

active proctype Master()  {
  

robstewart57

/////////////
// Before
syntax check
  the model contains 7 never claims: never_6, never_5, never_4, never_3, never_2, never_1, never_0
spin -a -o3 model.pml
  the model contains 7 never claims: never_6, never_5, never_4, never_3, never_2, never_1, never_0
  only one claim is used in a verification run
  choose which one with ./pan -N name (defaults to -N never_0)
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DNOREDUCE -w -o pan pan.c
./pan -m10000  -a -c1 -N never_6

robstewart57

{-# LANGUAGE ScopedTypeVariables #-}

import Control.Concurrent.MVar

class Foo a where
  mkFoo :: IO a
  readFoo :: a -> IO Int
  operateOnFoo :: a -> IO ()
  
newtype Bar = Bar (MVar Int)

robstewart57

-- API Module: Transport API as typeclass
class Transport t where
  createTransport :: IO (Either IOException t)
  newEndPoint     :: t -> IO (Either (TransportError NewEndPointErrorCode) EndPoint)
  closeTransport  :: t -> IO ()



-- Separate module: TCP implementation
newtype TCPTransport = TCPTransport (N.HostName,N.ServiceName,MVar TransportState,TCPParameters)

robstewart57

.....	.....
.....	.....

robstewart57

### FIRST RUN
cci: only keeping CTP list: (null)
cci: In sock post_load
cci: In tcp post_load
cci: entering ctp_sock_init
cci: querying interface en0 info with socket ioctls and ethtool...
cci: adding device [en0] (transport sock)
cci: exiting  ctp_sock_init
cci: entering ctp_tcp_init
cci: querying interface en0 info with socket ioctls and ethtool...

robstewart57

-module(ammunition_factory).
-export([repeat_explosion/2,time_bomb/1]).

time_bomb(0) -> exit("boom!");
time_bomb(N) ->
  timer:sleep(1000),
  time_bomb(N-1).

repeat_explosion(0,N) ->
  _Pid = spawn_monitor(fun() -> time_bomb(N) end),