BlackBox.hs

{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
#ifdef LIQUID
{-# OPTIONS_GHC -fplugin=LiquidHaskell
                -fplugin-opt=LiquidHaskell:--prune-unsorted
                -fplugin-opt=LiquidHaskell:--no-termination #-}
{- HLINT ignore "Use error" -}
#endif

{- | This module defines the BlackBox type class as well as the Automaton and SUL
sub classes.
-}
module Haal.BlackBox (
    Automaton (..),
    SUL (..),
    Finite,
    FiniteEq,
    FiniteOrd,
    inputs,
    outputs,
    walk,
    queryChecked,
    stepPure,
    walkPure,
    resetPure,
    initial,
    distinguish,
    accessSequences,
    localCharacterizingSet,
    globalCharacterizingSet,
    reachable,
    difference,
)
where

import Control.Exception (ErrorCall (..), throw)
import Control.Monad.Identity (Identity, runIdentity)
import qualified Data.Bifunctor as Bif
import qualified Data.List as List
import qualified Data.Map as Map
import Data.Maybe (fromMaybe)
import qualified Data.Set as Set

{- | The 'SUL' type class defines the basic interface for a black box automaton.
It provides methods to step through the automaton and reset it to its initial state.
It also requires a monad m, that may be 'Identity' in case of a pure SUL, or 'IO'
in case of an external program that performs IO.

Active automata learning requires queries to be independent, so the library
calls 'reset' before every membership query and every equivalence test case
(see 'query'). 'reset' must therefore bring the system back to its initial
state, and the library always continues with the value that 'reset' and 'step'
return. This supports two kinds of SULs:

* persistent ones, such as pure automata, where 'step' returns a new value and
  leaves the old one unchanged;
* stateful ones, such as a driver for a running process or a socket, where
  'step' and 'reset' change the external system and may return the same handle.
-}
class (Monad m) => SUL sul m where
    step :: sul i o -> i -> m (sul i o, o)
    reset :: sul i o -> m (sul i o)
    {-# MINIMAL step, reset #-}

    -- | Run a single query: reset the SUL, then feed it the inputs and collect the
    --     outputs. Every query the library sends to a SUL goes through this method, so
    --     that queries are independent of each other.
    --
    --     Override it when a SUL can answer a whole query more efficiently than step by
    --     step, e.g. by sending the whole word in one message. An override must:
    --
    --     * start from the initial state, like 'reset' does;
    --     * return exactly one output per input;
    --     * agree with 'reset' followed by 'walk'.
    --
    --     The library checks the number of outputs at runtime (see 'queryChecked').
    query :: sul i o -> [i] -> m [o]
    query sul is = do
        sul' <- reset sul
        (_, os) <- walk sul' is
        pure os

{- | 'query', checking that the SUL returned exactly one output per input.
A 'SUL' instance may override 'query', and the learners rely on this property,
so they query through this function. A violation is a bug in the instance and
fails with an error naming the expected and actual number of outputs.
-}

{-@ queryChecked :: (SUL sul m) => sul i o -> xs:[i] -> m {ys:[o] | len ys == len xs} @-}
queryChecked :: (SUL sul m) => sul i o -> [i] -> m [o]
queryChecked sul xs = do
    os <- query sul xs
    if length os == length xs
        then pure os
        else contractViolation (length xs) (length os)

{- | Fail because a 'query' override broke its contract. Unlike an @impossible@
error, this one is reachable. LiquidHaskell gives 'error' a @false@ precondition,
so this throws an t'ErrorCall' directly instead, which behaves the same at runtime.
-}
contractViolation :: Int -> Int -> a
contractViolation expected actual =
    throw . ErrorCall $
        "Haal.BlackBox.queryChecked: the SUL returned "
            ++ show actual
            ++ " outputs for a query of "
            ++ show expected
            ++ " inputs; an overridden 'query' must return one output per input"

-- | Finite is an alias for (Enum, Bounded).
type Finite i = (Enum i, Bounded i)

-- | FiniteEq is an alias for (Eq, Finite).
type FiniteEq i = (Eq i, Finite i)

-- | FiniteOrd is an alias for (Ord, Finite).
type FiniteOrd i = (Ord i, Finite i)

-- | Generalization of 'step' that operates on a list of inputs.

{-@ walk :: (SUL sul m) => sul i o -> xs:[i] -> m (sul i o, {ys:[o] | len ys == len xs}) @-}
walk :: (SUL sul m) => sul i o -> [i] -> m (sul i o, [o])
walk sul [] = pure (sul, [])
walk sul (x : xs) = do
    (sul', o) <- step sul x
    (sul'', os) <- walk sul' xs
    pure (sul'', o : os)

{-@ rangeIN :: (Enum i, Bounded i) => sul i o -> {is:[i] | len is > 0} @-}
rangeIN :: (Finite i) => sul i o -> [i]
rangeIN _ = minBound : [succ minBound .. maxBound]

{-@ rangeOUT :: (Enum o, Bounded o) => sul i o -> {os:[o] | len os > 0} @-}
rangeOUT :: (Finite o) => sul i o -> [o]
rangeOUT _ = minBound : [succ minBound .. maxBound]

{-@ assume Set.fromList :: Ord a => xs:[a] -> {s:Set.Set a | len xs > 0 => Set.size s > 0} @-}

-- | Return a Set containing only the valid inputs of the SUL.

{-@ inputs :: (Ord i, Enum i, Bounded i) => sul i o -> {is:Set.Set i | Set.size is > 0} @-}
inputs :: (FiniteOrd i) => sul i o -> Set.Set i
inputs x = Set.fromList $ rangeIN x

-- | Return a Set containing only the valid outputs of the SUL.

{-@ outputs :: (Ord o, Enum o, Bounded o) => sul i o -> {os:Set.Set o | Set.size os > 0} @-}
outputs :: (FiniteOrd o) => sul i o -> Set.Set o
outputs x = Set.fromList $ rangeOUT x

{- | The 'Automaton' type class extends the 'SUL' type class and adds
support for automata operations. Automatons are models, not programs,
so they are pure and operate in the Identity monad.
-}
class (SUL (aut s) Identity) => Automaton aut s where
    transitions ::
        (FiniteOrd i, FiniteOrd s) =>
        aut s i o ->
        Map.Map (s, i) (s, o)
    states :: (FiniteOrd s) => aut s i o -> Set.Set s
    current :: aut s i o -> s
    update :: aut s i o -> s -> aut s i o

-- | Pure instance of 'step'.
stepPure :: (SUL sul Identity) => sul i o -> i -> (sul i o, o)
stepPure sul i = runIdentity (step sul i)

-- | Pure instance of 'walk'.

{-@ walkPure :: (SUL sul Identity) => sul i o -> is:[i] -> (sul i o, {os:[o] | len os == len is})@-}
walkPure :: (SUL sul Identity) => sul i o -> [i] -> (sul i o, [o])
walkPure sul i = runIdentity (walk sul i)

-- | Pure instance of 'reset'.
resetPure :: (SUL sul Identity) => sul i o -> sul i o
resetPure sul = runIdentity (reset sul)

-- | Return the initial state of an automaton.
initial :: (Automaton aut s) => aut s i o -> s
initial = current . resetPure

-- | Return the set of reachable states of an automaton.
reachable :: forall s i o aut. (Automaton aut s, Ord s, FiniteOrd i) => aut s i o -> Set.Set s
reachable aut = bfs [initial aut] $ Set.singleton (initial aut)
  where
    alphabet = inputs aut

    bfs :: [s] -> Set.Set s -> Set.Set s
    bfs [] visited = visited
    bfs (st : queue) visited = bfs queue' visited'
      where
        aut' = update aut st
        neighbours = Set.map (current . fst . stepPure aut') alphabet
        visited' = visited `Set.union` neighbours
        queue' = Set.toList (neighbours `Set.difference` visited) ++ queue

-- | Returns a map containing the shortest sequence to access each reachable state from the initial state.
accessSequences ::
    forall s i o aut.
    (Automaton aut s, FiniteOrd i, Ord s) =>
    aut s i o ->
    Map.Map s [i]
accessSequences aut = bfs [(initialSt, [])] (Set.singleton initialSt) (Map.singleton initialSt [])
  where
    alphabet = Set.toList (inputs aut)
    initialSt = initial aut

    bfs :: [(s, [i])] -> Set.Set s -> Map.Map s [i] -> Map.Map s [i]
    bfs [] _ acc = Map.map List.reverse acc
    bfs ((_, prefix) : rest) visited acc =
        bfs (rest ++ newQueue) newVisited newMap
      where
        mo = fst $ walkPure (resetPure aut) (reverse prefix)
        successors =
            [ (nextState, input : prefix)
            | input <- alphabet
            , let nextState = current . fst $ stepPure mo input
            , nextState `Set.notMember` visited
            ]

        newMap = foldr (uncurry Map.insert) acc successors
        newVisited = foldr (Set.insert . fst) visited successors
        newQueue = successors

differenceFrom ::
    ( FiniteOrd i
    , FiniteOrd s
    , FiniteOrd s'
    , Eq o
    , Automaton aut1 s
    , Automaton aut2 s'
    ) =>
    aut1 s i o ->
    s ->
    aut2 s' i o ->
    s' ->
    Maybe [i]
differenceFrom aut1 s1 aut2 s2 = explore Map.empty [(s1, s2, [])]
  where
    alphabet = Set.toList (inputs aut1)
    stepAndCurrent mo i = Bif.first current (stepPure mo i)

    explore _ [] = Nothing
    explore visited ((q1, q2, prefix) : queue) =
        if (q1, q2) `Map.member` visited
            then explore visited queue
            else case discrepancy of
                Just symbol -> Just $ reverse (symbol : prefix)
                Nothing -> explore newVisited (queue ++ newQueue)
      where
        newVisited = Map.insert (q1, q2) prefix visited
        mo1 = update aut1 q1
        mo2 = update aut2 q2
        (nextStates1, outputs1) = unzip $ map (stepAndCurrent mo1) alphabet
        (nextStates2, outputs2) = unzip $ map (stepAndCurrent mo2) alphabet

        discrepancy = snd <$> List.find fst (zip (zipWith (/=) outputs1 outputs2) alphabet)

        appended = map (: prefix) alphabet

        toBeVisited = Map.fromList $ zip (zip nextStates1 nextStates2) appended
        newQueue = [(s1', s2', p) | ((s1', s2'), p) <- Map.toList toBeVisited, (s1', s2') `Map.notMember` visited]

{- | Finds a distinguishing sequence between two automata starting from their
 - initial states.
-}
difference ::
    ( FiniteOrd i
    , FiniteOrd s
    , FiniteOrd s'
    , Eq o
    , Automaton aut1 s
    , Automaton aut2 s'
    ) =>
    aut1 s i o ->
    aut2 s' i o ->
    Maybe [i]
difference aut1 aut2 = differenceFrom aut1 (initial aut1) aut2 (initial aut2)

{- | Returns an input sequence that distinguishes the given states in
the given automaton.
-}

{-@ distinguish :: (Automaton aut s, FiniteOrd i, Ord s, Eq o) =>
      aut s i o ->
      s1:s ->
      s2:s ->
      {is:[i] | s1 == s2 ==> len is = 0}
@-}
distinguish ::
    ( Automaton aut s
    , FiniteOrd s
    , FiniteOrd i
    , Eq o
    ) =>
    aut s i o ->
    s ->
    s ->
    [i]
distinguish _ s1 s2 | s1 == s2 = []
distinguish m s1 s2 = fromMaybe [] $ differenceFrom m s1 m s2

{- | Returns a set of lists of inputs that can be used to distinguish between the given state and
- any other state of the automaton.
-}
localCharacterizingSet ::
    ( Automaton aut s
    , FiniteOrd i
    , FiniteOrd s
    , Eq o
    ) =>
    aut s i o ->
    s ->
    Set.Set [i]
localCharacterizingSet m s = Set.fromList [d s sx | sx <- Set.toList $ states m, s /= sx]
  where
    d = distinguish m

{- | Returns a set of lists of inputs that can be used to distinguish between any two different states
of the automaton.
-}
globalCharacterizingSet ::
    ( Automaton aut s
    , FiniteOrd i
    , FiniteOrd s
    , Eq o
    ) =>
    aut s i o ->
    Set.Set [i]
globalCharacterizingSet m = Set.fromList [d s1 s2 | s1 <- sts, s2 <- sts, s1 < s2]
  where
    sts = Set.toList $ states m
    d = distinguish m