{- Joel Kelso (c) University of Western Australia 2003 -}

{-
module Fischer(
  ) where
-}

import List (intersperse,sort,(\\),isSuffixOf,isPrefixOf)
import Dict
import DictSet
import CircalLTS
import Structures
import Test
import StructureToXCircal
import MuEquiv

--
-- Fischer-protocol basic sequence with named transitions
-- but no constraints
--

plainFischerSort :: String
plainFischerSort = "ab,bc,cd,ca,da"

plainFischer :: String -> Process
plainFischer prefix = behave ("Fischer"++prefix) "a"
  (s plainFischerSort)
  [("a",s "ab","b"),("b",s "bc","c"),("c",s "cd","d"),
  ("c",s "ca","a"),("d",s "da","a")] where
    s = prefixAll prefix

--
-- Fischer-protocol basic sequence with named transitions
-- and register interaction.  Assumes the register is name "k" and the
-- empty register state is called "Z".  The shared actions
-- (the ones using the Z state) are prefixed by this process's
-- name (eg "Pk==Z" rather than "k==Z") to allow asynchronous
-- access to the register from multiple processes.
--

fischerTrans :: String
fischerTrans = "ab,bc,cd,ca,da"

fischer :: String -> Process
fischer nm = behave ("Fischer"++nm) "a"
  (sort ((prefixAll nm "ab,bc,ca,cd,da") ++ 
    [nm++"k==Z",nm++"k:=Z","k=="++nm,"k!="++nm,"k:="++nm]))
  [("a",sort [nm++"ab",nm++"k==Z"],"b"),
   ("b",sort [nm++"bc","k:="++nm],"c"),
   ("c",sort [nm++"cd","k=="++nm],"d"),
   ("c",sort [nm++"ca","k!="++nm],"a"),
   ("d",sort [nm++"da",nm++"k:=Z"],"a")]

--
-- Register is parameterised by register name (eg "k") and
-- the name of its states (eg "a","b" etc).  It has actions
--   k:=a k:=b ... for setting state
--   k==a k==b ... for reading state
--   k!=a k!=b ... for reading state
-- Start state is the first one mentioned in state list.
--

register :: String -> [String] -> Process
register nm sts = behave ("register"++nm) (head sts)
  (sort $ registerEvents nm sts)
  ([(s,[nm++"=="++s],s) | s <- sts] ++
  [(s1,[nm++"!="++s2],s1) | s1 <- sts, s2 <- sts, s1 /= s2] ++
  [(s1,[nm++":="++s2],s2) | s1 <- sts, s2 <- sts])

registerEvents :: String -> [String] -> [String]
registerEvents k ps = [re++p | 
  re <- [k++"==",k++":=",k++"!="], p <- ps]

--
-- This process allows independant access to a set of events
-- from a set of processes, each of which define their own
-- access methods.  This is necessary, for example, to allow
-- multiple processes to read and write a register without
-- having to synchronise.
-- This one does exclusive multiporting - only one process
-- at a time.
--

multiport :: [String] -> [String] -> Process
multiport evs ps = behave ("multiport"++concat evs++concat ps) "P"
  (sort (evs++multiportEvents evs ps))
  [("P",sort [ev,p++ev],"P") | ev <- evs, p <- ps]

multiportEvents :: [String] -> [String] -> Sort Action
multiportEvents evs ps = sort [p++ev | ev <- evs, p <- ps]

--
-- System building functions
--

sharedActions :: [String]
sharedActions = ["k==Z","k:=Z"]

-- here we abstract all the register events

fischerSystem :: [String] -> Process
fischerSystem pfxs = abstract (
  multiportEvents sharedActions pfxs ++ 
  registerEvents "k" ("Z":pfxs)) $
  compose [
   fischerWorkers pfxs,
   register "k" ("Z" : pfxs),
   multiport sharedActions pfxs]

-- A version without the register for comparison

f1 pfxs = abstract (
  multiportEvents sharedActions pfxs ++ 
  registerEvents "k" ("Z":pfxs)) $
  compose [
   fischerWorkers pfxs ]

fischerWorkers :: [String] -> Process
fischerWorkers pfxs = compose [fischer p | p <- pfxs]

fischerEvents :: [String] -> [Action]
fischerEvents pfxs = 
  sort $ concat [prefixAll p plainFischerSort | p <- pfxs]

--
-- Analysis process - project out only events entering
-- and leaving critical section.
--

csView :: [String] -> Process -> Process
csView pfxs = abstract ((fischerEvents pfxs) \\
  (concat [[pfx++"cd",pfx++"da"] | pfx <- pfxs]))

--
-- Mutual exclusion property process
--

-- don't use "Z" as a process name
mutexP :: (String,String) -> [String] -> Process
mutexP (enter,leave) ps = let
    evs = [p++e | e <- [enter,leave], p <- ps]
  in behave ("MutexP"++cmfy evs) "Z"
  (sort evs)
  (concat [[("Z",[p++enter],p),(p,[p++leave],"Z")] |
    p <- ps])

pqTest = mutexP ("cd","da") ["P","Q"]

--
-- Timing constraint.  This is supposed to encapsulate the
-- timing constraint enforced by the Fischer worker's transitions
-- guarded by their clocks.
--

timeConstraints :: [String] -> Process
timeConstraints ps = compose [timeConstraint p q | p <- ps, q <- ps, p /= q]

{-
timeConstraint :: String -> String -> Process
timeConstraint p q = nonsequence ("Timing"++p++"_"++q)
  (sort [q++"ab",p++"bc",p++"cd",q++"bc"])
  [q++"ab",p++"bc",p++"cd"]
-}

timeConstraint :: String -> String -> Process
timeConstraint p q = nonsequence ("Timing"++p++"_"++q)
  (sort [q++"ab",p++"cd",q++"bc"])
  [q++"ab",p++"cd"]

constrainedSystem :: [String] -> Process
constrainedSystem ps = compose [fischerSystem ps,timeConstraints ps]

--
-- Process tools
--

matchPos :: (Eq a) => [a] -> [a] -> Int
matchPos trg seq = maximum
  [length seq - n | n <- [0..length seq], drop n seq `isPrefixOf` trg]

nonsequence :: String -> [Action] -> [Action] -> Process
nonsequence name srt seq = behave name "S1"
  (sort srt)
  (concat [transitionsFrom n | n <- [1..length seq]]) where
    dest l n = 1 + (matchPos seq ((take (n-1) seq)++[l]))
    transitionsFrom n = [("S"++show n,[l],"S"++(show $ dest l n)) | 
      l <- srt, dest l n <= length seq]

prefixAll :: String -> String -> Event Action
prefixAll pref spec = map (pref ++) (sfs spec)

cmfy :: [Action] -> String
cmfy as = concat $ intersperse "," as

desynchroniser :: [Action] -> Process
desynchroniser as = behave ("Desync"++cmfy as) "P"
  (sort as) [("P",[a],"P") | a <- as]

desynchronise :: [Action] -> Process -> Process
desynchronise as p = compose [p,desynchroniser as]

without :: Int -> [a] -> [a]
without 0 (x:xs) = xs
without n (x:xs) = x : without (n-1) xs

--
-- Equivalence checking entry points
--

-- Write out XTC code to do check
xCircalTest ps =
  writeFile "test.xtc" $ writeEquivCheck 
    ("L", csView ps $ constrainedSystem ps)
    ("R", mutexP ("cd","da") ps)
    "may_eq"

-- Do check with Haskell Circal equiv check engine
hCircalTest ps =
  eqvt (csView ps $ constrainedSystem ps)
       (mutexP ("cd","da") ps)

-- This reveals that the prototype Haskell Circal BDD equiv
-- checking engine is (a) slow and (b) broken.
bddCircalTest ps =
  equivCheck 
    (csView ps $ constrainedSystem ps)
    (mutexP ("cd","da") ps)

main = do

--  Print out critical-section view of constrained sytem:
--  mcadtest $ csView ["P","Q"] $ constrainedSystem ["P","Q"]

--  Write out XTC code for equiv check:
--  xCircalTest ["P","Q"]

--  Try experimental BDD engine:
--  putStrLn $ show $ bddCircalTest ["P","Q"]

--  Equiv check using Haskell Circal engine:
    putStrLn $ hCircalTest ["P","Q"]