diff --git a/CHANGELOG b/CHANGELOG deleted file mode 100644 --- a/CHANGELOG +++ /dev/null @@ -1,45 +0,0 @@ -1.0.0.1 => 1.1 -============== -This package version is now compatible with the command-line application for -the ICCMA competition. See: https://github.com/nebasuke/DungICCMA and the -competition website: http://argumentationcompetition.org/2015/index.html - -This package has again been significantly extended and now includes: - -* Strict version of the grounded fixpoint semantics. - -* Definitions of what it means to be a preferred and stable extension. - -* Naive implementations of complete, preferred and stable semantics using - the characteristic function. The fixpoint definitions are actually FASTER - than the fancy algorithm implementation. - -* Included the fast implementations of intersect, nub and (\\) by Niklas - Hambuechen. - -* Added some clarifying text for the "complete" labelling. - - -1.0 => 1.0.0.1 -============== -* Fixed the record declaration in Main.hs. - -* Added an example file. - -0.9 => 1.0 -============= -This package version is now compatible with the translation package CarneadesIntoDung. -See http://hackage.haskell.org/package/CarneadesIntoDung/ - -This package has furthermore been significantly extended and now includes: - -* Preferred, stable and semi-stable semantics along with all definitions from - Caminada's paper "An Algorithm for Computing Semi-Stable Semantics". - -* An Input module, allowing files in standard CEGARTIX/PrefSat format to be parsed. - -* An Output module, allowing AFs in this package to be outputted in standard - CEGARTIX/PrefSat format. - -* A main executable, allowing input files to be read, argumentation frameworks - to be outputted and evaluated. diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,64 @@ +# Changelog + +## 1.1 → 2.0.0.0 + +### Breaking changes + +- **Fixed `groundedF` infinite-loop bug**: `groundedF` now correctly applies + the characteristic function at each step instead of recursing with unchanged + arguments. Code relying on `groundedF'` as a workaround can switch back to + `groundedF`. + +- **CLI rewritten**: The `dungell` executable now uses `optparse-applicative` + instead of `cmdargs`. Command-line flags have changed: + - Semantics are selected via `--grounded`, `--preferred`, `--stable`, + `--semi-stable`, or `--all` + +### Improvements + +- Upgraded to `cabal-version: 3.0` format +- Relaxed `containers` upper bound to build on GHC 9.4+ +- Added `Language.Dung` convenience re-export module +- Added test suite (tasty + QuickCheck + doctest) +- Added GitHub Actions CI for GHC 9.4, 9.6, 9.8, 9.10 +- Fixed all `-Wall` warnings +- Removed dependency on unmaintained `cmdargs` library +- Converted documentation to Markdown + +## 1.0.0.1 → 1.1 + +This package version is now compatible with the command-line application for +the ICCMA competition. See: and the +competition website: + +This package has again been significantly extended and now includes: + +- Strict version of the grounded fixpoint semantics. +- Definitions of what it means to be a preferred and stable extension. +- Naive implementations of complete, preferred and stable semantics using + the characteristic function. The fixpoint definitions are actually FASTER + than the fancy algorithm implementation. +- Included the fast implementations of `intersect`, `nub` and `(\\)` by + Niklas Hambuechen. +- Added some clarifying text for the "complete" labelling. + +## 1.0 → 1.0.0.1 + +- Fixed the record declaration in Main.hs. +- Added an example file. + +## 0.9 → 1.0 + +This package version is now compatible with the translation package +CarneadesIntoDung. See + +This package has furthermore been significantly extended and now includes: + +- Preferred, stable and semi-stable semantics along with all definitions from + Caminada's paper "An Algorithm for Computing Semi-Stable Semantics". +- An Input module, allowing files in standard CEGARTIX/PrefSat format to be + parsed. +- An Output module, allowing AFs in this package to be outputted in standard + CEGARTIX/PrefSat format. +- A main executable, allowing input files to be read, argumentation frameworks + to be outputted and evaluated. diff --git a/Dung.cabal b/Dung.cabal --- a/Dung.cabal +++ b/Dung.cabal @@ -1,48 +1,102 @@ +cabal-version: 3.0 name: Dung -category: Argumentation, Embedded, AI -version: 1.1 -license: BSD3 -cabal-version: >= 1.6 +version: 2.0.0.0 +license: BSD-3-Clause license-file: LICENSE author: Bas van Gijzel -maintainer: Bas van Gijzel +maintainer: Bas van Gijzel +copyright: Copyright (C) 2014-2026 Bas van Gijzel stability: experimental -homepage: http://www.cs.nott.ac.uk/~bmv/Dung/ -copyright: Copyright (C) 2014 Bas van Gijzel +category: Argumentation, Embedded, AI +homepage: https://github.com/nebasuke/Dung synopsis: An implementation of the Dung argumentation frameworks. -description: An implementation of Dung's argumentation frameworks, an abstract argumentation model used to either directly represent conflicting information, or used as - a translation target for more complex (structured) argumentation models. For an introduction to Dung's frameworks see - and Dung's paper from 1995: \"On the acceptability of arguments and its fundamental role - in nonmonotonic reasoning, logic programming, and n-person games\", Artificial Intelligence 77: 321-357. - For the papers accompanying this library see \"Towards a framework for the implementation and verification of translations between argumentation - models\" and \"A principled approach to the implementation of argumentation models\", available at . +description: + An implementation of Dung's argumentation frameworks, an abstract + argumentation model used to either directly represent conflicting + information, or used as a translation target for more complex (structured) + argumentation models. For an introduction to Dung's frameworks see + and Dung's paper + from 1995: \"On the acceptability of arguments and its fundamental role + in nonmonotonic reasoning, logic programming, and n-person games\", + Artificial Intelligence 77: 321-357. + For the papers accompanying this library see \"Towards a framework for + the implementation and verification of translations between argumentation + models\" and \"A principled approach to the implementation of argumentation + models\", available at . build-type: Simple +tested-with: GHC == 9.4.8, GHC == 9.6.6, GHC == 9.8.4, GHC == 9.10.1 -Extra-Source-Files: - CHANGELOG - exampleaf.txt +extra-doc-files: + README.md + CHANGELOG.md -Library - build-depends: - base >= 4 && < 5, - containers >= 0.3 && < 0.6, - cmdargs >= 0.10.2, - parsec >= 3 +extra-source-files: + LICENSE + exampleaf.txt + dungex.txt - hs-source-dirs: - src +source-repository head + type: git + location: https://github.com/nebasuke/Dung +common warnings + ghc-options: + -Wall + -Wcompat + -Widentities + -Wincomplete-record-updates + -Wincomplete-uni-patterns + -Wredundant-constraints + default-language: Haskell2010 + +library + import: warnings + hs-source-dirs: src + build-depends: + base >= 4.16 && < 5, + containers >= 0.6 && < 0.8, + parsec >= 3.1 && < 3.2 exposed-modules: + Language.Dung Language.Dung.AF Language.Dung.Examples - Language.Dung.Output Language.Dung.Input + Language.Dung.Output -Executable dungell - main-Is: Main.hs - hs-source-dirs: src +executable dungell + import: warnings + main-is: Main.hs + hs-source-dirs: app + build-depends: + base >= 4.16 && < 5, + Dung, + optparse-applicative >= 0.17 && < 0.19 + ghc-options: -threaded -source-repository head - Type: git - Location: https://github.com/nebasuke/Dung +test-suite dung-tests + import: warnings + type: exitcode-stdio-1.0 + main-is: Main.hs + hs-source-dirs: test + build-depends: + base >= 4.16 && < 5, + Dung, + containers >= 0.6 && < 0.8, + tasty >= 1.4 && < 1.6, + tasty-hunit >= 0.10 && < 0.11, + tasty-quickcheck >= 0.10 && < 0.11, + QuickCheck >= 2.14 && < 2.16 + other-modules: + Test.Language.Dung.AF + Test.Language.Dung.Input + Test.Language.Dung.Properties + +test-suite dung-doctest + import: warnings + type: exitcode-stdio-1.0 + main-is: Doctest.hs + hs-source-dirs: test + build-depends: + base >= 4.16 && < 5, + doctest >= 0.20 && < 0.23 diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,4 +1,4 @@ -Copyright (c)2014, 2015, Bas van Gijzel +Copyright (c) 2014-2026, Bas van Gijzel All rights reserved. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,53 @@ +# Dung + +An implementation of Dung's argumentation frameworks, an abstract argumentation +model used to either directly represent conflicting information, or used as +a translation target for more complex (structured) argumentation models. + +For an introduction to Dung's frameworks see the +[Wikipedia article on argumentation frameworks](http://en.wikipedia.org/wiki/Argumentation_framework) +and Dung's paper from 1995: + +> "On the acceptability of arguments and its fundamental role in nonmonotonic +> reasoning, logic programming, and n-person games", Artificial Intelligence +> 77: 321-357. + +For the papers accompanying this library see: + +- "Towards a framework for the implementation and verification of translations + between argumentation models" +- "A principled approach to the implementation of argumentation models" + +Available at . + +## Usage + +```haskell +import Language.Dung + +-- Define an argumentation framework: A -> B -> C +let af = AF ["A", "B", "C"] [("A", "B"), ("B", "C")] + +-- Compute the grounded extension +groundedExt af +-- ["A", "C"] + +-- Compute preferred extensions +preferredExt af +-- [["A","C"]] +``` + +## Executable + +The `dungell` executable reads argumentation frameworks from files in +CEGARTIX/PrefSat format: + +``` +dungell --filename exampleaf.txt --grounded +dungell --filename exampleaf.txt --preferred +dungell --filename exampleaf.txt --all +``` + +## License + +BSD-3-Clause. See [LICENSE](LICENSE) for details. diff --git a/Setup.hs b/Setup.hs deleted file mode 100644 --- a/Setup.hs +++ /dev/null @@ -1,2 +0,0 @@ -import Distribution.Simple -main = defaultMain diff --git a/app/Main.hs b/app/Main.hs new file mode 100644 --- /dev/null +++ b/app/Main.hs @@ -0,0 +1,98 @@ +-- |This module implements a command-line interface to the implementation of +-- Dung's argumentation frameworks. Dung + Haskell = Dungell +{-# LANGUAGE RecordWildCards #-} +module Main + ( main + ) where + +import Language.Dung.AF (groundedExt, preferredExt, stableExt, semiStableExt, + DungAF(..)) +import Language.Dung.Input +import Language.Dung.Output + +import Options.Applicative +import System.Exit +import Control.Monad (when) + +data Semantics + = Grounded + | Preferred + | Stable + | SemiStable + deriving (Eq, Show) + +data Options = Options + { optLaxCegartix :: Bool + , optFileName :: FilePath + , optOutputFile :: Maybe FilePath + , optSemantics :: [Semantics] + } deriving (Show) + +semanticsFlags :: Parser [Semantics] +semanticsFlags = combineFlags + <$> switch (long "grounded" <> help "Output grounded extension for the AF") + <*> switch (long "preferred" <> help "Output preferred extensions for the AF") + <*> switch (long "stable" <> help "Output stable extensions for the AF") + <*> switch (long "semi-stable" <> help "Output semi-stable extensions for the AF") + <*> switch (long "all" <> help "Output extensions of all implemented semantics for AF") + where + combineFlags gr pr st ss allSem + | allSem = [Grounded, Preferred, Stable, SemiStable] + | otherwise = concat + [ [Grounded | gr] + , [Preferred | pr] + , [Stable | st] + , [SemiStable | ss] + ] + +optionsParser :: Parser Options +optionsParser = Options + <$> switch + ( long "lax-cegartix" + <> help "Output in lax CEGARTIX/PrefSat format (+parentheses)" + ) + <*> strOption + ( long "filename" + <> metavar "FILE" + <> help "Name of the file to be read" + ) + <*> optional (strOption + ( long "outputfile" + <> metavar "FILE" + <> help "Name of the file to be written" + )) + <*> semanticsFlags + +opts :: ParserInfo Options +opts = info (optionsParser <**> helper) + ( fullDesc + <> progDesc "An implementation of Dung's AFs" + <> header "dungell - Dung + Haskell argumentation framework tool" + ) + +main :: IO () +main = do + Options{..} <- execParser opts + input <- readFile optFileName + af <- case parseAF input of + Left err -> do + putStrLn "Parsing error: " + print err + exitWith (ExitFailure 1) + Right af -> return af + exec optLaxCegartix optOutputFile optSemantics af + +exec :: (Show arg, Ord arg) + => Bool -> Maybe FilePath -> [Semantics] -> DungAF arg -> IO () +exec laxCegartix outputFile semantics af = do + print af + when (Grounded `elem` semantics) $ putStr "grounded: " >> print (groundedExt af) + when (Preferred `elem` semantics) $ putStr "preferred: " >> print (preferredExt af) + when (Stable `elem` semantics) $ putStr "stable: " >> print (stableExt af) + when (SemiStable `elem` semantics) $ putStr "semi-stable: " >> print (semiStableExt af) + case outputFile of + Nothing -> return () + Just fp -> + if not laxCegartix + then writeFile fp (toStrictCegartix af) >> putStrLn "File outputted." + else writeFile fp (toCegartix af) >> putStrLn "File outputted." diff --git a/dungex.txt b/dungex.txt new file mode 100644 --- /dev/null +++ b/dungex.txt @@ -0,0 +1,15 @@ +arg("a"). +arg("b"). +arg("c"). +arg("d"). +arg("e"). +arg("f"). +arg("g"). +att("a","b"). +att("c","b"). +att("c","d"). +att("d","c"). +att("d","e"). +att("e","g"). +att("f","e"). +att("g","f"). diff --git a/exampleaf.txt b/exampleaf.txt --- a/exampleaf.txt +++ b/exampleaf.txt @@ -1,15 +1,15 @@ -arg(a). -arg(b). -arg(c). -arg(d). -arg(e). -arg(f). -arg(g). -att(a,b). -att(c,b). -att(c,d). -att(d,c). -att(d,e). -att(e,g). -att(f,e). +arg(a). +arg(b). +arg(c). +arg(d). +arg(e). +arg(f). +arg(g). +att(a,b). +att(c,b). +att(c,d). +att(d,c). +att(d,e). +att(e,g). +att(f,e). att(g,f). diff --git a/src/Language/Dung.hs b/src/Language/Dung.hs new file mode 100644 --- /dev/null +++ b/src/Language/Dung.hs @@ -0,0 +1,12 @@ +-- | Convenience re-export module for Dung's argumentation frameworks. +-- +-- This module re-exports "Language.Dung.AF" so users can simply write: +-- +-- @ +-- import Language.Dung +-- @ +module Language.Dung + ( module Language.Dung.AF + ) where + +import Language.Dung.AF diff --git a/src/Language/Dung/AF.hs b/src/Language/Dung/AF.hs --- a/src/Language/Dung/AF.hs +++ b/src/Language/Dung/AF.hs @@ -1,515 +1,515 @@ --- | This module implements Dung's argumentation frameworks. -module Language.Dung.AF - ( - -- * Basic definitions - DungAF(..), - setAttacks, aplus, amin, argplus, argmin, - conflictFree, acceptable, f, admissible, - -- * Grounded, complete, preferred and stable semantics through fixpoints - groundedF, groundedF', completeF, preferredF, stableF, - -- * Definitions of a preferred and stable extension - isPreferredExt, isStableExt, - -- * Basic labelling definitions - -- |The following functions are implementations of the - -- definitions in \"An algorithm for Computing Semi-Stable - -- Semantics\" in \"Symbolic and Quantitative Approaches to Reasoning with - -- Uncertainty\", pages 222--234, Springer, 2007. - Status(..), Labelling(..), - inLab, outLab, undecLab, - allIn, allOut, allUndec, - powerLabel, - unattacked, attacked, - labAttackers, illegallyIn, illegallyOut, illegallyUndec, - legallyIn, legallyOut, legallyUndec, - isAdmissible, isComplete, isPreferred, isStable, isSemiStable, - transitionStep, terminatedTransition, superIllegallyIn, - -- * Grounded, preferred, semi-stable and stable labellings - -- |The following functions are implementations of the - -- definitions in \"An algorithm for Computing Semi-Stable - -- Semantics\" in \"Symbolic and Quantitative Approaches to Reasoning with - -- Uncertainty\", pages 222--234, Springer, 2007 and Section 4.1 of Proof - -- Theories and Algorithms for Abstract Argumentation Frameworks by Modgil - -- and Caminada. - grounded, groundedExt, complete, preferred, stable, semiStable, - completeExt, preferredExt, stableExt, semiStableExt - ) - where -import Data.List (partition, delete, sort) --- For the implementation of intersect, (\\) and nub -import qualified Data.Set as Set -import qualified Data.Map.Strict as Map --- import Prelude hiding ((\\)) - --- Haskell library's intersect, (\\) and nub only require an Eq instance. --- If we have an Ord instance as well, it can be sped up significantly. --- I therefore use intersect, (\\) and nub from https://github.com/nh2/haskell-ordnub --- by Niklas Hambuechen -intersect :: (Ord a) => [a] -> [a] -> [a] -intersect a b = filter (`Set.member` bSet) a - where - bSet = Set.fromList b - -nub :: (Ord a) => [a] -> [a] -nub = go Set.empty - where - go _ [] = [] - go s (x:xs) = if x `Set.member` s then go s xs - else x : go (Set.insert x s) xs - -infix 5 \\ - -(\\) :: (Ord a) => [a] -> [a] -> [a] -a \\ b = go initHist a - where - initHist = Map.fromListWith (+) [ (x, 1 :: Int) | x <- b ] - - go _ [] = [] - go hist (x:xs) = case Map.lookup x hist of - Just n | n > 0 -> go (Map.insert x (n-1) hist) xs - _ -> x : go hist xs - --- |An abstract argumentation framework is a set of arguments --- (represented as a list) and an attack relation on these arguments. -data DungAF arg = AF [arg] [(arg, arg)] - deriving (Eq, Ord, Show) - --- |Given an argumentation framework, determines whether args --- (subset of the arguments in the AF), attacks an argument arg (in the AF). -setAttacks :: Eq arg => DungAF arg -> [arg] -> arg -> Bool -setAttacks (AF _ def) args arg - = or [b == arg | (a, b) <- def, a `elem` args] - --- |Given an argumentation framework, determines the set of arguments --- that are attacked by an argument (in the AF). -aplus :: Eq arg => DungAF arg -> arg -> [arg] -aplus (AF args atk) a = [b | (a', b) <- atk, a == a'] - --- |Given an argumentation framework, determines the set of arguments --- attacking an argument (in the AF). -amin :: Eq arg => DungAF arg -> arg -> [arg] -amin (AF args atk) a = [b | (b, a') <- atk, a == a'] - --- |Given an argumentation framework, determines the set of arguments --- that are attacked by the given subset of arguments (in the AF). -argplus :: Ord arg => DungAF arg -> [arg] -> [arg] -argplus af = nub . concatMap (aplus af) - --- |Given an argumentation framework, determines the set of arguments --- that attack a given subset of arguments (in the AF). -argmin :: Ord arg => DungAF arg -> [arg] -> [arg] -argmin af = nub . concatMap (amin af) - --- |Given an argumentation framework, determines whether args --- (subset of the arguments in the AF) is conflict-free. -conflictFree :: Eq arg => DungAF arg -> [arg] -> Bool -conflictFree (AF _ def) args - = null [(a,b) | (a, b) <- def, a `elem` args, b `elem` args] - --- |Given an argumentation framework, determines whether an --- argument is acceptable with respect to a list of 'args' (subset of the arguments in the AF). -acceptable :: Eq arg => DungAF arg -> arg -> [arg] -> Bool -acceptable af@(AF _ def) a args - = and [setAttacks af args b | (b, a') <- def, a == a'] - --- |Given an argumentation framework, returns the set of arguments --- that are acceptable with respect to 'args' (subset of the arguments in the AF). -f :: Eq arg => DungAF arg -> [arg] -> [arg] -f af@(AF args' _) args = [a | a <- args', acceptable af a args] - --- Returns 'True' if 'xs' is a subset of 'ys' -subset :: Ord a => [a] -> [a] -> Bool -xs `subset` ys = null (xs \\ ys) - --- |Given an argumentation framework, determines whether --- the set of arguments 'args' (subset of the arguments in the AF) is admissible, --- i.e. if 'args' is 'conflictFree' and args is a subset of @f af args@ -admissible :: Ord arg => DungAF arg -> [arg] -> Bool -admissible af args = conflictFree af args && args `subset` f af args - --- alternatively: --- if 'args' is 'conflictFree' and each argument in args is acceptable with --- respect to args. --- admissible af args = conflictFree af args && --- and [acceptable af arg args | arg <- args] - -------------------------------------------------------------------------------- ---- Implementations of semantics through fixpoints or generation of complete--- ---- extensions --- -------------------------------------------------------------------------------- - --- |Given a characteristic function f, computes the grounded extension --- by iterating on the empty set (list) until it reaches a fixpoint. -groundedF :: Eq arg => ([arg] -> [arg]) -> [arg] -groundedF f = step f [] - where step f args - | f args == args = args - | otherwise = step f args - --- |Given a characteristic function f, computes the grounded extension --- by iterating on the empty set (list) until it reaches a fixpoint. --- Strict version. -groundedF' :: Eq arg => ([arg] -> [arg]) -> [arg] -groundedF' f = step f [] - where step f args - | f args == args = args - | otherwise = - let args' = f args - in args' `seq` step f args' - --- Computes the powerset of a list. -powerset :: [a] -> [[a]] -powerset [] = [[]] -powerset (x:xs) = powerset xs ++ map (x:) (powerset xs) - --- |Given an argumentation framework, computes all complete extension, --- by taking all sets of arguments of the powerset of arguments of that AF, --- given that they are admissible and @f af == f@. -completeF :: Ord arg => DungAF arg -> [[arg]] -completeF af@(AF args _) = - let fAF = f af - in filter (\ x -> admissible af x && x == fAF x) (powerset args) - --- |Given an argumentation framework, computes all preferred extensions, --- by applying a filter on the complete extensions. Note that this, --- naive definition is faster than the current algorithm implementation. -preferredF :: Ord arg => DungAF arg -> [[arg]] -preferredF af@(AF args _) = - let cs = completeF af - in filter (isPreferredExt af cs) cs - --- |Given an argumentation framework, computes all stable extensions, --- by applying a filter on the complete extensions. Note that this, --- naive definition is faster than the current algorithm implementation. -stableF :: Ord arg => DungAF arg -> [[arg]] -stableF af@(AF args _) = - let ps = preferredF af - in filter (isStableExt af) ps - --- |A complete extension is also a preferred extension if it is not a --- subset of one of the other extensions. -isPreferredExt :: Ord arg => DungAF arg -> [[arg]] -> [arg] -> Bool -isPreferredExt af exts ext = all (not . (ext `subset`)) - (delete ext exts) - --- |S is a stable extension is an extension iff it is equal to the set --- of arguments not attacked by S. -isStableExt :: Ord arg => DungAF arg -> [arg] -> Bool -isStableExt af@(AF args _) ext = filter (unattacked (args \\ ext) af) args == ext - -------------------------------------------------------------------------- --- The following functions are implementations of the --- definitions in \"An algorithm for Computing Semi-Stable --- Semantics\" in \"Symbolic and Quantitative Approaches to --- Reasoning with Uncertainty\", pages 222--234, Springer, 2007. -------------------------------------------------------------------------------- - --- |Labelling status of arguments. -data Status = In | Out | Undecided - deriving (Eq, Show, Ord) - --- Definition 4 --- |Labelling of arguments. -type Labelling arg = [(arg,Status)] - - --- Just below Definition 4, functions on a labelling: --- in(Lab) --- |Given a labelling of arguments, give back the arguments labelled 'In'. -inLab :: Labelling arg -> [arg] -inLab labs = [a | (a, In) <- labs] - --- out(Lab) --- |Given a labelling of arguments, give back the arguments labelled 'Out'. -outLab :: Labelling arg -> [arg] -outLab labs = [a | (a, Out) <- labs] - --- undec(lab) --- |Given a labelling of arguments, give back the arguments labelled --- 'Undecided'. -undecLab :: Labelling arg -> [arg] -undecLab labs = [a | (a, Undecided) <- labs] - - --- Just below Definition 4, Caminada distinguishes three special kinds of labelling. - --- |The allIn labelling is a 'Labelling' that labels every argument 'In'. -allIn :: [arg] -> Labelling arg -allIn = map (\ a -> (a, In)) - --- |The allOut labelling is a 'Labelling' that labels every argument 'Out'. -allOut :: [arg] -> Labelling arg -allOut = map (\ a -> (a, Out)) - --- |The allUndec labelling is a 'Labelling' that labels every argument 'Undecided'. -allUndec :: [arg] -> Labelling arg -allUndec = map (\ a -> (a, Undecided)) - --- |Given a list of arguments that are 'Out' in an argumentation framework af, --- an argument 'arg' is unattacked if the list of its attackers, ignoring the outs, is empty. -unattacked :: Ord arg => [arg] -> - DungAF arg -> arg -> Bool -unattacked outs (AF _ def) arg = - let attackers = [a | (a, b) <- def, arg == b] - in null (attackers \\ outs) - --- |Given a list of arguments that are 'In' in an argumentation framework af, --- an argument 'arg' is attacked if there exists an attacker that is 'In'. -attacked :: Ord arg => [arg] -> - DungAF arg -> arg -> Bool -attacked ins (AF _ def) arg = - let attackers = [a | (a, b) <- def, arg == b] - in not (null (attackers `intersect` ins)) - --- |Computes a list with all possible labellings. -powerLabel :: [arg] -> [Labelling arg] -powerLabel [] = [[]] -powerLabel (x:xs) = map ((x,In):) (powerLabel xs) - ++ map ((x,Out):) (powerLabel xs) - ++ map ((x,Undecided):) (powerLabel xs) ------- - --- |Computes the grounded labelling for a Dung argumentation framework, --- returning a (unique) list of arguments with statuses. --- --- Based on section 4.1 of Proof Theories and Algorithms for Abstract Argumentation Frameworks --- by Modgil and Caminada. -grounded :: Ord arg => DungAF arg -> Labelling arg -grounded af@(AF args _) = grounded' [] [] args af - where - grounded' :: Ord a => [a] -> [a] -> - [a] -> DungAF a -> [(a, Status)] - grounded' ins outs [] _ - = allIn ins - ++ allOut outs - grounded' ins outs args af = - let newIns = filter (unattacked outs af) args - newOuts = filter (attacked ins af) args - in if null (newIns ++ newOuts) - then allIn ins - ++ allOut outs - ++ allUndec args - else grounded' (ins ++ newIns) - (outs ++ newOuts) - (args \\ (newIns ++ newOuts)) - af - --- |The grounded extension of an argumentation framework is just the grounded labelling, --- keeping only those arguments that were labelled 'In'. -groundedExt :: Ord arg => DungAF arg -> [arg] -groundedExt af = [arg | (arg, In) <- grounded af] - --- |Given an argumentation framework, determines the list of attackers of an argument, --- from a given labelling, returning the labelled attackers. -labAttackers :: Eq arg => DungAF arg -> arg -> Labelling arg -> Labelling arg -labAttackers (AF args atk) a labs = [lab | lab@(b, _) <- labs, (b, a) `elem` atk] - --- Definition 5.1 of Caminada --- |Given an AF and 'Labelling', --- an argument a (in the AF) is illegally 'In' iff a is labelled 'In', --- but not all its attackers are labelled 'Out'. -illegallyIn :: Eq arg => DungAF arg -> Labelling arg -> (arg, Status) -> Bool -illegallyIn af labs (a, In) = not . null $ [lab | lab@(_, l) <- labAttackers af a labs, l /= Out] -illegallyIn _ _ _ = False - --- Definition 5.2 of Caminada --- |Given an AF and 'Labelling', --- an argument a (in the AF) is illegally 'Out' iff a is labelled 'Out' --- but does not have an attacker labelled 'In'. -illegallyOut :: Eq arg => DungAF arg -> Labelling arg -> (arg, Status) -> Bool -illegallyOut af labs (a, Out) = null [lab | lab@(_, In) <- labAttackers af a labs] -illegallyOut _ _ _ = False - --- Definition 5.3 of Caminada --- |Given an AF and 'Labelling', --- an argument a (in the AF) is illegally 'Undecided' iff a is labelled 'Undecided' --- but either all its attackers are labelled 'Out' --- or it has an attacker that is labelled 'In'. -illegallyUndec :: Eq arg => DungAF arg -> Labelling arg -> (arg, Status) -> Bool -illegallyUndec af labs (a, Undecided) = and [l == Out | (_, l) <- labAttackers af a labs] - || (not . null) [lab | lab@(_, In) <- labAttackers af a labs] -illegallyUndec _ _ _ = False - - --- Just below Definition 5.3 of Caminada --- The implementation of a 'Labelling' that has no illegal --- arguments is given as 'isComplete', further below. - --- Just below Definition 5.3 of Caminada --- |Given an AF and 'Labelling', --- an argument a (in the AF) is legally 'In' iff a is labelled 'In' --- and it's not 'illegallyIn'. -legallyIn :: Eq arg => DungAF arg -> Labelling arg -> (arg, Status) -> Bool -legallyIn af labs arg@(_, In) = not $ illegallyIn af labs arg -legallyIn _ _ _ = False - --- Just below Definition 5.3 of Caminada --- |Given an AF and 'Labelling', --- an argument a (in the AF) is legally 'Out' iff a is labelled 'Out' --- and it's not 'illegallyOut'. -legallyOut :: Eq arg => DungAF arg -> Labelling arg -> (arg, Status) -> Bool -legallyOut af labs arg@(_, Out) = not $ illegallyOut af labs arg -legallyOut _ _ _ = False - --- Just below Definition 5.3 of Caminada --- |Given an AF and 'Labelling', --- an argument a (in the AF) is legally 'Undecided' iff a is labelled 'Undecided' --- and it's not 'illegallyUndec'. -legallyUndec :: Eq arg => DungAF arg -> Labelling arg -> (arg, Status) -> Bool -legallyUndec af labs arg@(_, Undecided) = not $ illegallyUndec af labs arg -legallyUndec _ _ _ = False - --- Definition 6 of Caminada --- |Given an AF, an admissible labelling is a 'Labelling' without arguments --- that are 'illegallyIn' and without arguments that are 'illegallyOut'. -isAdmissible :: Eq arg => DungAF arg -> Labelling arg -> Bool -isAdmissible af labs = null $ - [lab | lab@(a, In) <- labs, illegallyIn af labs lab] - ++ [lab | lab@(a, Out) <- labs, illegallyOut af labs lab] - --- Definition 7 of Caminada --- |Given an AF, a complete labelling is a labelling without arguments --- that are 'illegallyIn', without arguments that are 'illegallyOut' and --- without arguments that are 'illegallyUndec'. -isComplete :: Eq arg => DungAF arg -> Labelling arg -> Bool -isComplete af labs = null $ - [lab | lab@(a, In) <- labs, illegallyIn af labs lab] - ++ [lab | lab@(a, Out) <- labs, illegallyOut af labs lab] - ++ [lab | lab@(a, Undecided) <- labs, illegallyUndec af labs lab] - - --- Definition 8 of Caminada, grounded labelling --- |Let 'labs' be a complete labelling, i.e. @isComplete af labs@, we say that --- labs is a grounded labelling iff @inLab labs@ is minimal --- (w.r.t. set inclusion). -isGrounded :: Ord arg => DungAF arg -> [Labelling arg] -> Labelling arg -> Bool -isGrounded af labss labs = isComplete af labs && - all (inLab labs `subset`) (map inLab labss) - --- Definition 8 of Caminada, preferred labelling --- |Let 'labs' be a complete labelling, i.e. @isComplete af labs@, we say that --- labs is a preferred labelling iff @inLab labs@ is maximal --- (w.r.t. set inclusion). -isPreferred :: Ord arg => DungAF arg -> [Labelling arg] -> Labelling arg -> Bool -isPreferred af labss labs = isComplete af labs && - all (not . (inLab labs `subset` )) - (map inLab (delete labs labss)) - --- Definition 8 of Caminada, stable labelling --- |Let 'labs' be a complete labelling, i.e. 'isComplete af labs', we say that --- labs is a preferred labelling iff @undecLab(labs) == []@ -isStable :: Eq arg => DungAF arg -> [Labelling arg] -> Labelling arg -> Bool -isStable af labss labs = isComplete af labs && - null (undecLab labs) - --- Definition 8 of Caminada, semi-stable labelling --- |Let 'labs' be a complete labelling, i.e. @isComplete af labs@, we say that --- labs is a semi-stable labelling iff @undecLab labs@ is minimal --- (w.r.t. set inclusion). -isSemiStable :: Ord arg => DungAF arg -> [Labelling arg] -> Labelling arg -> Bool -isSemiStable af labss labs = isComplete af labs && - all (undecLab labs `subset`) - (map undecLab labss) - --- Definition 9 of Caminada --- |Given an AF, a labelling labs and an illegally in argument a in the af, --- (i.e. @illegallyIn af a labs@ => True), --- a transition step on a in labs consists of the following: --- 1. the label of a is changed from 'In' to 'Out' --- 2. for every b in {a} \cup a+, if b is illegally out, --- then change the label from b from 'Out' to 'Undecided' -transitionStep :: Eq arg => DungAF arg -> Labelling arg -> arg -> Labelling arg -transitionStep af labs a = - let labs' = (a, Out) : delete (a, In) labs -- Step 1 - bs = a : aplus af a -- bs = every b in {a} \cup a+ - (newUndecs, rem) = partition (\ lab@(b, l) -> - b `elem` bs - && illegallyOut af labs' lab) - labs' - in map (\ (a, _) -> (a, Undecided)) newUndecs - ++ rem - - --- Based on Definition 10 of Caminada --- Instead of checking termination of a transition sequence --- This function implements a check of termination for a specific transition --- last . --- |Given an AF, a labelling, labs, is terminated iff labs does not contain any argument that is --- illegally in, i.e. @not (illegallyIn af lab arg)@ for all arg in labs. -terminatedTransition :: Eq arg => DungAF arg -> Labelling arg -> Bool -terminatedTransition af labs = not . or $ map (illegallyIn af labs) labs - --- Definition 11 of Caminada --- |Given an AF and 'Labelling', --- an argument a (in the AF) is superillegally 'In' iff a is labelled 'In', --- and it is attacked by an argument that is legally 'In' or legally 'Undecided'. -superIllegallyIn :: Eq arg => DungAF arg -> Labelling arg -> (arg, Status) -> Bool -superIllegallyIn af labs (a, In) = - not . null $ - [lab | lab <- labAttackers af a labs, - legallyIn af labs lab || legallyUndec af labs lab] -superIllegallyIn _ _ _ = False - --- Based on the Algorithm of Caminada --- Instead of using a search tree and keeping a list of potential semi-stable --- labellings, we remove the checks. --- Note that this actually gives us an algorithm for computing at least the --- maximal and minimal complete labellings, allowing us to then filter out --- the grounded, preferred, stable or semi-stable labellings dependent on --- what should be maximal or minimal. --- |Computes maximal and minimal complete labellings for a Dung argumentation --- framework. This is based on Caminada's algorithm for computing semi-stable --- labellings, with all checks removed. -complete :: Ord arg => DungAF arg -> [Labelling arg] -complete af@(AF args atk) = - let allInArgs = allIn args - complete' :: Eq arg => DungAF arg -> Labelling arg -> [Labelling arg] - complete' af labs = - case filter (superIllegallyIn af labs) labs of - [] -> case filter (illegallyIn af labs) labs of - [] -> [labs] - ills -> concatMap (complete' af) $ - map (transitionStep af labs . fst) - ills - ((a,_) : _) -> complete' af (transitionStep af labs a) - in nub . map sort $ complete' af allInArgs - --- |Computes all preferred labellings for a Dung argumentation framework, by --- taking the maximally in complete labellings. -preferred :: Ord arg => DungAF arg -> [Labelling arg] -preferred af@(AF args atk) = - let completes = complete af - in filter (isPreferred af completes) completes - --- |Computes all stable labellings for a Dung argumentation framework, by --- keeping only those labellings with no 'Undecided' labels. -stable :: Ord arg => DungAF arg -> [Labelling arg] -stable af@(AF args atk) = - let completes = complete af - in filter (isStable af completes) completes - --- |Computes all semi-stable labellings for a Dung argumentation framework, by --- taking the minimally undecided complete labellings. -semiStable :: Ord arg => DungAF arg -> [Labelling arg] -semiStable af@(AF args atk) = - let completes = complete af - in filter (isSemiStable af completes) completes - --- |The complete extension of an argumentation framework is just the complete labelling, --- keeping only those arguments that were labelled 'In'. -completeExt :: Ord arg => DungAF arg -> [[arg]] -completeExt af = [[arg | (arg, In) <- c] | c <- complete af] - --- |The preferred extension of an argumentation framework is just the preferred labelling, --- keeping only those arguments that were labelled 'In'. -preferredExt :: Ord arg => DungAF arg -> [[arg]] -preferredExt af = [[arg | (arg, In) <- c] | c <- preferred af] - --- |The stable extension of an argumentation framework is just the stable labelling, --- keeping only those arguments that were labelled 'In'. -stableExt :: Ord arg => DungAF arg -> [[arg]] -stableExt af = [[arg | (arg, In) <- c] | c <- stable af] - --- |The semi-stable extension of an argumentation framework is just the semi-stable labelling, --- keeping only those arguments that were labelled 'In'. -semiStableExt :: Ord arg => DungAF arg -> [[arg]] +-- | This module implements Dung's argumentation frameworks. +module Language.Dung.AF + ( + -- * Basic definitions + DungAF(..), + setAttacks, aplus, amin, argplus, argmin, + conflictFree, acceptable, f, admissible, + -- * Grounded, complete, preferred and stable semantics through fixpoints + groundedF, groundedF', completeF, preferredF, stableF, + -- * Definitions of a preferred and stable extension + isPreferredExt, isStableExt, + -- * Basic labelling definitions + -- |The following functions are implementations of the + -- definitions in \"An algorithm for Computing Semi-Stable + -- Semantics\" in \"Symbolic and Quantitative Approaches to Reasoning with + -- Uncertainty\", pages 222--234, Springer, 2007. + Status(..), Labelling, + inLab, outLab, undecLab, + allIn, allOut, allUndec, + powerLabel, + unattacked, attacked, + labAttackers, illegallyIn, illegallyOut, illegallyUndec, + legallyIn, legallyOut, legallyUndec, + isAdmissible, isComplete, isGrounded, isPreferred, isStable, isSemiStable, + transitionStep, terminatedTransition, superIllegallyIn, + -- * Grounded, preferred, semi-stable and stable labellings + -- |The following functions are implementations of the + -- definitions in \"An algorithm for Computing Semi-Stable + -- Semantics\" in \"Symbolic and Quantitative Approaches to Reasoning with + -- Uncertainty\", pages 222--234, Springer, 2007 and Section 4.1 of Proof + -- Theories and Algorithms for Abstract Argumentation Frameworks by Modgil + -- and Caminada. + grounded, groundedExt, complete, preferred, stable, semiStable, + completeExt, preferredExt, stableExt, semiStableExt + ) + where +import Data.List (partition, delete, sort) +-- For the implementation of intersect, (\\) and nub +import qualified Data.Set as Set +import qualified Data.Map.Strict as Map +-- import Prelude hiding ((\\)) + +-- Haskell library's intersect, (\\) and nub only require an Eq instance. +-- If we have an Ord instance as well, it can be sped up significantly. +-- I therefore use intersect, (\\) and nub from https://github.com/nh2/haskell-ordnub +-- by Niklas Hambuechen +intersect :: (Ord a) => [a] -> [a] -> [a] +intersect a b = filter (`Set.member` bSet) a + where + bSet = Set.fromList b + +nub :: (Ord a) => [a] -> [a] +nub = go Set.empty + where + go _ [] = [] + go s (x:xs) = if x `Set.member` s then go s xs + else x : go (Set.insert x s) xs + +infix 5 \\ + +(\\) :: (Ord a) => [a] -> [a] -> [a] +a \\ b = go initHist a + where + initHist = Map.fromListWith (+) [ (x, 1 :: Int) | x <- b ] + + go _ [] = [] + go hist (x:xs) = case Map.lookup x hist of + Just n | n > 0 -> go (Map.insert x (n-1) hist) xs + _ -> x : go hist xs + +-- |An abstract argumentation framework is a set of arguments +-- (represented as a list) and an attack relation on these arguments. +data DungAF arg = AF [arg] [(arg, arg)] + deriving (Eq, Ord, Show) + +-- |Given an argumentation framework, determines whether args +-- (subset of the arguments in the AF), attacks an argument arg (in the AF). +setAttacks :: Eq arg => DungAF arg -> [arg] -> arg -> Bool +setAttacks (AF _ def) args arg + = or [b == arg | (a, b) <- def, a `elem` args] + +-- |Given an argumentation framework, determines the set of arguments +-- that are attacked by an argument (in the AF). +aplus :: Eq arg => DungAF arg -> arg -> [arg] +aplus (AF _args atk) a = [b | (a', b) <- atk, a == a'] + +-- |Given an argumentation framework, determines the set of arguments +-- attacking an argument (in the AF). +amin :: Eq arg => DungAF arg -> arg -> [arg] +amin (AF _args atk) a = [b | (b, a') <- atk, a == a'] + +-- |Given an argumentation framework, determines the set of arguments +-- that are attacked by the given subset of arguments (in the AF). +argplus :: Ord arg => DungAF arg -> [arg] -> [arg] +argplus af = nub . concatMap (aplus af) + +-- |Given an argumentation framework, determines the set of arguments +-- that attack a given subset of arguments (in the AF). +argmin :: Ord arg => DungAF arg -> [arg] -> [arg] +argmin af = nub . concatMap (amin af) + +-- |Given an argumentation framework, determines whether args +-- (subset of the arguments in the AF) is conflict-free. +conflictFree :: Eq arg => DungAF arg -> [arg] -> Bool +conflictFree (AF _ def) args + = null [(a,b) | (a, b) <- def, a `elem` args, b `elem` args] + +-- |Given an argumentation framework, determines whether an +-- argument is acceptable with respect to a list of 'args' (subset of the arguments in the AF). +acceptable :: Eq arg => DungAF arg -> arg -> [arg] -> Bool +acceptable af@(AF _ def) a args + = and [setAttacks af args b | (b, a') <- def, a == a'] + +-- |Given an argumentation framework, returns the set of arguments +-- that are acceptable with respect to 'args' (subset of the arguments in the AF). +f :: Eq arg => DungAF arg -> [arg] -> [arg] +f af@(AF args' _) args = [a | a <- args', acceptable af a args] + +-- Returns 'True' if 'xs' is a subset of 'ys' +subset :: Ord a => [a] -> [a] -> Bool +xs `subset` ys = null (xs \\ ys) + +-- |Given an argumentation framework, determines whether +-- the set of arguments 'args' (subset of the arguments in the AF) is admissible, +-- i.e. if 'args' is 'conflictFree' and args is a subset of @f af args@ +admissible :: Ord arg => DungAF arg -> [arg] -> Bool +admissible af args = conflictFree af args && args `subset` f af args + +-- alternatively: +-- if 'args' is 'conflictFree' and each argument in args is acceptable with +-- respect to args. +-- admissible af args = conflictFree af args && +-- and [acceptable af arg args | arg <- args] + +------------------------------------------------------------------------------- +--- Implementations of semantics through fixpoints or generation of complete--- +--- extensions --- +------------------------------------------------------------------------------- + +-- |Given a characteristic function f, computes the grounded extension +-- by iterating on the empty set (list) until it reaches a fixpoint. +groundedF :: Eq arg => ([arg] -> [arg]) -> [arg] +groundedF f = step f [] + where step f args + | f args == args = args + | otherwise = step f (f args) + +-- |Given a characteristic function f, computes the grounded extension +-- by iterating on the empty set (list) until it reaches a fixpoint. +-- Strict version. +groundedF' :: Eq arg => ([arg] -> [arg]) -> [arg] +groundedF' f = step f [] + where step f args + | f args == args = args + | otherwise = + let args' = f args + in args' `seq` step f args' + +-- Computes the powerset of a list. +powerset :: [a] -> [[a]] +powerset [] = [[]] +powerset (x:xs) = powerset xs ++ map (x:) (powerset xs) + +-- |Given an argumentation framework, computes all complete extension, +-- by taking all sets of arguments of the powerset of arguments of that AF, +-- given that they are admissible and @f af == f@. +completeF :: Ord arg => DungAF arg -> [[arg]] +completeF af@(AF args _) = + let fAF = f af + in filter (\ x -> admissible af x && x == fAF x) (powerset args) + +-- |Given an argumentation framework, computes all preferred extensions, +-- by applying a filter on the complete extensions. Note that this, +-- naive definition is faster than the current algorithm implementation. +preferredF :: Ord arg => DungAF arg -> [[arg]] +preferredF af = + let cs = completeF af + in filter (isPreferredExt af cs) cs + +-- |Given an argumentation framework, computes all stable extensions, +-- by applying a filter on the complete extensions. Note that this, +-- naive definition is faster than the current algorithm implementation. +stableF :: Ord arg => DungAF arg -> [[arg]] +stableF af = + let ps = preferredF af + in filter (isStableExt af) ps + +-- |A complete extension is also a preferred extension if it is not a +-- subset of one of the other extensions. +isPreferredExt :: Ord arg => DungAF arg -> [[arg]] -> [arg] -> Bool +isPreferredExt _af exts ext = all (not . (ext `subset`)) + (delete ext exts) + +-- |S is a stable extension is an extension iff it is equal to the set +-- of arguments not attacked by S. +isStableExt :: Ord arg => DungAF arg -> [arg] -> Bool +isStableExt af@(AF args _) ext = filter (unattacked (args \\ ext) af) args == ext + +------------------------------------------------------------------------- +-- The following functions are implementations of the +-- definitions in \"An algorithm for Computing Semi-Stable +-- Semantics\" in \"Symbolic and Quantitative Approaches to +-- Reasoning with Uncertainty\", pages 222--234, Springer, 2007. +------------------------------------------------------------------------------- + +-- |Labelling status of arguments. +data Status = In | Out | Undecided + deriving (Eq, Show, Ord) + +-- Definition 4 +-- |Labelling of arguments. +type Labelling arg = [(arg,Status)] + + +-- Just below Definition 4, functions on a labelling: +-- in(Lab) +-- |Given a labelling of arguments, give back the arguments labelled 'In'. +inLab :: Labelling arg -> [arg] +inLab labs = [a | (a, In) <- labs] + +-- out(Lab) +-- |Given a labelling of arguments, give back the arguments labelled 'Out'. +outLab :: Labelling arg -> [arg] +outLab labs = [a | (a, Out) <- labs] + +-- undec(lab) +-- |Given a labelling of arguments, give back the arguments labelled +-- 'Undecided'. +undecLab :: Labelling arg -> [arg] +undecLab labs = [a | (a, Undecided) <- labs] + + +-- Just below Definition 4, Caminada distinguishes three special kinds of labelling. + +-- |The allIn labelling is a 'Labelling' that labels every argument 'In'. +allIn :: [arg] -> Labelling arg +allIn = map (\ a -> (a, In)) + +-- |The allOut labelling is a 'Labelling' that labels every argument 'Out'. +allOut :: [arg] -> Labelling arg +allOut = map (\ a -> (a, Out)) + +-- |The allUndec labelling is a 'Labelling' that labels every argument 'Undecided'. +allUndec :: [arg] -> Labelling arg +allUndec = map (\ a -> (a, Undecided)) + +-- |Given a list of arguments that are 'Out' in an argumentation framework af, +-- an argument 'arg' is unattacked if the list of its attackers, ignoring the outs, is empty. +unattacked :: Ord arg => [arg] -> + DungAF arg -> arg -> Bool +unattacked outs (AF _ def) arg = + let attackers = [a | (a, b) <- def, arg == b] + in null (attackers \\ outs) + +-- |Given a list of arguments that are 'In' in an argumentation framework af, +-- an argument 'arg' is attacked if there exists an attacker that is 'In'. +attacked :: Ord arg => [arg] -> + DungAF arg -> arg -> Bool +attacked ins (AF _ def) arg = + let attackers = [a | (a, b) <- def, arg == b] + in not (null (attackers `intersect` ins)) + +-- |Computes a list with all possible labellings. +powerLabel :: [arg] -> [Labelling arg] +powerLabel [] = [[]] +powerLabel (x:xs) = map ((x,In):) (powerLabel xs) + ++ map ((x,Out):) (powerLabel xs) + ++ map ((x,Undecided):) (powerLabel xs) +------ + +-- |Computes the grounded labelling for a Dung argumentation framework, +-- returning a (unique) list of arguments with statuses. +-- +-- Based on section 4.1 of Proof Theories and Algorithms for Abstract Argumentation Frameworks +-- by Modgil and Caminada. +grounded :: Ord arg => DungAF arg -> Labelling arg +grounded af@(AF args _) = grounded' [] [] args af + where + grounded' :: Ord a => [a] -> [a] -> + [a] -> DungAF a -> [(a, Status)] + grounded' ins outs [] _ + = allIn ins + ++ allOut outs + grounded' ins outs args af = + let newIns = filter (unattacked outs af) args + newOuts = filter (attacked ins af) args + in if null (newIns ++ newOuts) + then allIn ins + ++ allOut outs + ++ allUndec args + else grounded' (ins ++ newIns) + (outs ++ newOuts) + (args \\ (newIns ++ newOuts)) + af + +-- |The grounded extension of an argumentation framework is just the grounded labelling, +-- keeping only those arguments that were labelled 'In'. +groundedExt :: Ord arg => DungAF arg -> [arg] +groundedExt af = [arg | (arg, In) <- grounded af] + +-- |Given an argumentation framework, determines the list of attackers of an argument, +-- from a given labelling, returning the labelled attackers. +labAttackers :: Eq arg => DungAF arg -> arg -> Labelling arg -> Labelling arg +labAttackers (AF _args atk) a labs = [lab | lab@(b, _) <- labs, (b, a) `elem` atk] + +-- Definition 5.1 of Caminada +-- |Given an AF and 'Labelling', +-- an argument a (in the AF) is illegally 'In' iff a is labelled 'In', +-- but not all its attackers are labelled 'Out'. +illegallyIn :: Eq arg => DungAF arg -> Labelling arg -> (arg, Status) -> Bool +illegallyIn af labs (a, In) = not . null $ [()| (_, l) <- labAttackers af a labs, l /= Out] +illegallyIn _ _ _ = False + +-- Definition 5.2 of Caminada +-- |Given an AF and 'Labelling', +-- an argument a (in the AF) is illegally 'Out' iff a is labelled 'Out' +-- but does not have an attacker labelled 'In'. +illegallyOut :: Eq arg => DungAF arg -> Labelling arg -> (arg, Status) -> Bool +illegallyOut af labs (a, Out) = null [() | (_, In) <- labAttackers af a labs] +illegallyOut _ _ _ = False + +-- Definition 5.3 of Caminada +-- |Given an AF and 'Labelling', +-- an argument a (in the AF) is illegally 'Undecided' iff a is labelled 'Undecided' +-- but either all its attackers are labelled 'Out' +-- or it has an attacker that is labelled 'In'. +illegallyUndec :: Eq arg => DungAF arg -> Labelling arg -> (arg, Status) -> Bool +illegallyUndec af labs (a, Undecided) = and [l == Out | (_, l) <- labAttackers af a labs] + || (not . null) [() | (_, In) <- labAttackers af a labs] +illegallyUndec _ _ _ = False + + +-- Just below Definition 5.3 of Caminada +-- The implementation of a 'Labelling' that has no illegal +-- arguments is given as 'isComplete', further below. + +-- Just below Definition 5.3 of Caminada +-- |Given an AF and 'Labelling', +-- an argument a (in the AF) is legally 'In' iff a is labelled 'In' +-- and it's not 'illegallyIn'. +legallyIn :: Eq arg => DungAF arg -> Labelling arg -> (arg, Status) -> Bool +legallyIn af labs arg@(_, In) = not $ illegallyIn af labs arg +legallyIn _ _ _ = False + +-- Just below Definition 5.3 of Caminada +-- |Given an AF and 'Labelling', +-- an argument a (in the AF) is legally 'Out' iff a is labelled 'Out' +-- and it's not 'illegallyOut'. +legallyOut :: Eq arg => DungAF arg -> Labelling arg -> (arg, Status) -> Bool +legallyOut af labs arg@(_, Out) = not $ illegallyOut af labs arg +legallyOut _ _ _ = False + +-- Just below Definition 5.3 of Caminada +-- |Given an AF and 'Labelling', +-- an argument a (in the AF) is legally 'Undecided' iff a is labelled 'Undecided' +-- and it's not 'illegallyUndec'. +legallyUndec :: Eq arg => DungAF arg -> Labelling arg -> (arg, Status) -> Bool +legallyUndec af labs arg@(_, Undecided) = not $ illegallyUndec af labs arg +legallyUndec _ _ _ = False + +-- Definition 6 of Caminada +-- |Given an AF, an admissible labelling is a 'Labelling' without arguments +-- that are 'illegallyIn' and without arguments that are 'illegallyOut'. +isAdmissible :: Eq arg => DungAF arg -> Labelling arg -> Bool +isAdmissible af labs = null $ + [lab | lab@(_, In) <- labs, illegallyIn af labs lab] + ++ [lab | lab@(_, Out) <- labs, illegallyOut af labs lab] + +-- Definition 7 of Caminada +-- |Given an AF, a complete labelling is a labelling without arguments +-- that are 'illegallyIn', without arguments that are 'illegallyOut' and +-- without arguments that are 'illegallyUndec'. +isComplete :: Eq arg => DungAF arg -> Labelling arg -> Bool +isComplete af labs = null $ + [lab | lab@(_, In) <- labs, illegallyIn af labs lab] + ++ [lab | lab@(_, Out) <- labs, illegallyOut af labs lab] + ++ [lab | lab@(_, Undecided) <- labs, illegallyUndec af labs lab] + + +-- Definition 8 of Caminada, grounded labelling +-- |Let 'labs' be a complete labelling, i.e. @isComplete af labs@, we say that +-- labs is a grounded labelling iff @inLab labs@ is minimal +-- (w.r.t. set inclusion). +isGrounded :: Ord arg => DungAF arg -> [Labelling arg] -> Labelling arg -> Bool +isGrounded af labss labs = isComplete af labs && + all (inLab labs `subset`) (map inLab labss) + +-- Definition 8 of Caminada, preferred labelling +-- |Let 'labs' be a complete labelling, i.e. @isComplete af labs@, we say that +-- labs is a preferred labelling iff @inLab labs@ is maximal +-- (w.r.t. set inclusion). +isPreferred :: Ord arg => DungAF arg -> [Labelling arg] -> Labelling arg -> Bool +isPreferred af labss labs = isComplete af labs && + all (not . (inLab labs `subset` )) + (map inLab (delete labs labss)) + +-- Definition 8 of Caminada, stable labelling +-- |Let 'labs' be a complete labelling, i.e. 'isComplete af labs', we say that +-- labs is a stable labelling iff @undecLab(labs) == []@ +isStable :: Eq arg => DungAF arg -> [Labelling arg] -> Labelling arg -> Bool +isStable af _labss labs = isComplete af labs && + null (undecLab labs) + +-- Definition 8 of Caminada, semi-stable labelling +-- |Let 'labs' be a complete labelling, i.e. @isComplete af labs@, we say that +-- labs is a semi-stable labelling iff @undecLab labs@ is minimal +-- (w.r.t. set inclusion). +isSemiStable :: Ord arg => DungAF arg -> [Labelling arg] -> Labelling arg -> Bool +isSemiStable af labss labs = isComplete af labs && + all (undecLab labs `subset`) + (map undecLab labss) + +-- Definition 9 of Caminada +-- |Given an AF, a labelling labs and an illegally in argument a in the af, +-- (i.e. @illegallyIn af a labs@ => True), +-- a transition step on a in labs consists of the following: +-- 1. the label of a is changed from 'In' to 'Out' +-- 2. for every b in {a} \cup a+, if b is illegally out, +-- then change the label from b from 'Out' to 'Undecided' +transitionStep :: Eq arg => DungAF arg -> Labelling arg -> arg -> Labelling arg +transitionStep af labs a = + let labs' = (a, Out) : delete (a, In) labs -- Step 1 + bs = a : aplus af a -- bs = every b in {a} \cup a+ + (newUndecs, rest) = partition (\ lab@(b, _l) -> + b `elem` bs + && illegallyOut af labs' lab) + labs' + in map (\ (x, _) -> (x, Undecided)) newUndecs + ++ rest + + +-- Based on Definition 10 of Caminada +-- Instead of checking termination of a transition sequence +-- This function implements a check of termination for a specific transition +-- last . +-- |Given an AF, a labelling, labs, is terminated iff labs does not contain any argument that is +-- illegally in, i.e. @not (illegallyIn af lab arg)@ for all arg in labs. +terminatedTransition :: Eq arg => DungAF arg -> Labelling arg -> Bool +terminatedTransition af labs = not . or $ map (illegallyIn af labs) labs + +-- Definition 11 of Caminada +-- |Given an AF and 'Labelling', +-- an argument a (in the AF) is superillegally 'In' iff a is labelled 'In', +-- and it is attacked by an argument that is legally 'In' or legally 'Undecided'. +superIllegallyIn :: Eq arg => DungAF arg -> Labelling arg -> (arg, Status) -> Bool +superIllegallyIn af labs (a, In) = + not . null $ + [lab | lab <- labAttackers af a labs, + legallyIn af labs lab || legallyUndec af labs lab] +superIllegallyIn _ _ _ = False + +-- Based on the Algorithm of Caminada +-- Instead of using a search tree and keeping a list of potential semi-stable +-- labellings, we remove the checks. +-- Note that this actually gives us an algorithm for computing at least the +-- maximal and minimal complete labellings, allowing us to then filter out +-- the grounded, preferred, stable or semi-stable labellings dependent on +-- what should be maximal or minimal. +-- |Computes maximal and minimal complete labellings for a Dung argumentation +-- framework. This is based on Caminada's algorithm for computing semi-stable +-- labellings, with all checks removed. +complete :: Ord arg => DungAF arg -> [Labelling arg] +complete af@(AF args _atk) = + let allInArgs = allIn args + complete' :: Eq arg => DungAF arg -> Labelling arg -> [Labelling arg] + complete' af labs = + case filter (superIllegallyIn af labs) labs of + [] -> case filter (illegallyIn af labs) labs of + [] -> [labs] + ills -> concatMap (complete' af) $ + map (transitionStep af labs . fst) + ills + ((a,_) : _) -> complete' af (transitionStep af labs a) + in nub . map sort $ complete' af allInArgs + +-- |Computes all preferred labellings for a Dung argumentation framework, by +-- taking the maximally in complete labellings. +preferred :: Ord arg => DungAF arg -> [Labelling arg] +preferred af = + let completes = complete af + in filter (isPreferred af completes) completes + +-- |Computes all stable labellings for a Dung argumentation framework, by +-- keeping only those labellings with no 'Undecided' labels. +stable :: Ord arg => DungAF arg -> [Labelling arg] +stable af = + let completes = complete af + in filter (isStable af completes) completes + +-- |Computes all semi-stable labellings for a Dung argumentation framework, by +-- taking the minimally undecided complete labellings. +semiStable :: Ord arg => DungAF arg -> [Labelling arg] +semiStable af = + let completes = complete af + in filter (isSemiStable af completes) completes + +-- |The complete extension of an argumentation framework is just the complete labelling, +-- keeping only those arguments that were labelled 'In'. +completeExt :: Ord arg => DungAF arg -> [[arg]] +completeExt af = [[arg | (arg, In) <- c] | c <- complete af] + +-- |The preferred extension of an argumentation framework is just the preferred labelling, +-- keeping only those arguments that were labelled 'In'. +preferredExt :: Ord arg => DungAF arg -> [[arg]] +preferredExt af = [[arg | (arg, In) <- c] | c <- preferred af] + +-- |The stable extension of an argumentation framework is just the stable labelling, +-- keeping only those arguments that were labelled 'In'. +stableExt :: Ord arg => DungAF arg -> [[arg]] +stableExt af = [[arg | (arg, In) <- c] | c <- stable af] + +-- |The semi-stable extension of an argumentation framework is just the semi-stable labelling, +-- keeping only those arguments that were labelled 'In'. +semiStableExt :: Ord arg => DungAF arg -> [[arg]] semiStableExt af = [[arg | (arg, In) <- c] | c <- semiStable af] diff --git a/src/Language/Dung/Examples.hs b/src/Language/Dung/Examples.hs --- a/src/Language/Dung/Examples.hs +++ b/src/Language/Dung/Examples.hs @@ -1,321 +1,330 @@ --- | This is the examples module accompanying the implementation of Dung's --- argumentation frameworks. --- --- This module contains a collection of examples, showing how to define --- arguments, argumentation frameworks and how to use the standard definitions. --- --- To run these examples, or your own: start GHCi and do the following: --- --- @\:l Language.Dung.Examples@ --- -module Language.Dung.Examples - ( - -- * Example uses of the basic definitions - -- |Given @a = \"A\"@, @b = \"B\"@, @c = \"C\"@ - AbsArg, a, b, c, exampleAF, exampleAF2, - -- * Example uses of the fixpoint definitions - faf, - -- * Example uses of the basic labelling definitions - -- |Given @d = \"D\"@, @e = \"E\"@ - d, e, exampleAF3, exampleAF4, - -- * Example uses of the input functionality - exampleAF5, - -- * Example uses of the output functionality - output, output2, output3, output4, output5 - ) - where -import Language.Dung.AF -import Language.Dung.Input -import Language.Dung.Output --- | The simplest abstract argument is an argument identifiable by its name -type AbsArg = String - - -a, b, c :: AbsArg -a = "A" -b = "B" -c = "C" - --- |Example AF: A -> B -> C -exampleAF :: DungAF AbsArg -exampleAF = AF [a, b, c] [(a, b), (b, c)] - --- |Example AF: A \<-> B --- --- Now follow a few example outputs using the above argumentation frameworks. --- --- [setAttacks:] --- --- @[a,b]@ 'setAttacks' @c@ in the argumentation framework 'exampleAF': --- --- >>> setAttacks exampleAF [a,b] c --- True --- --- >>> setAttacks exampleAF [b,c] a --- False --- --- >>> setAttacks exampleAF2 [] b --- False --- --- [conflictFree:] --- --- @\[a,c\]@ is 'conflictFree' in the argumentation framework 'exampleAF': --- --- >>> conflictFree exampleAF [a,c] --- True --- --- >>> conflictFree exampleAF [a,b,c] --- False --- --- >>> conflictFree exampleAF2 [a,b] --- False --- --- [acceptable:] --- --- @c@ is acceptable w.r.t. @\[a,b\]@ in the argumentation framework 'exampleAF': --- --- >>> acceptable exampleAF c [a,b] --- True --- --- >>> acceptable exampleAF c [] --- False --- --- >>> acceptable exampleAF b [a,b,c] --- False --- --- [admissible:] --- --- @\[a,b,c\]@ is admissible in the argumentation framework 'exampleAF': --- --- >>> admissible exampleAF [a,b,c] --- False --- --- >>> admissible exampleAF [a,c] --- True --- --- >>> admissible exampleAF [a] --- True --- --- [grounded:] --- --- The grounded labelling of the argumentation frameworks 'exampleAF' --- and 'exampleAF2': --- --- >>> grounded exampleAF --- [("A",In),("C",In),("B",Out)] --- --- >>> grounded exampleAF2 --- [("A",Undecided),("B",Undecided)] --- --- [groundedExt:] --- --- The grounded extension of the argumentation frameworks 'exampleAF' --- and 'exampleAF2': --- --- >>> groundedExt exampleAF --- ["A", "C"] --- >>> groundedExt exampleAF2 --- [] -exampleAF2 :: DungAF AbsArg -exampleAF2 = AF [a, b] [(a, b), (b, a)] - --- |fixed point function for a specific argumentation framework, --- @faf = f exampleAF@. --- --- [groundedF:] --- --- The grounded extension of the argumentation framework 'exampleAF' using the --- fixpoint definition: --- --- >>> groundedF faf --- ["A","C"] --- --- >>> groundedF (f exampleAF2) --- [] -faf :: [AbsArg] -> [AbsArg] -faf = f exampleAF - -d, e :: AbsArg -d = "D" -e = "E" - --- |Left hand side of Fig1. in Caminada. --- Arguments are: {a,b,c,d}. --- Attacks: {(a, a), (a, c), (b, c), (c, d)} -exampleAF3 :: DungAF AbsArg -exampleAF3 = AF [a, b, c, d] [(a, a), (a, c), (b, c), (c, d)] - --- |Right hand side of Fig1. in Caminada. --- Arguments are: {a,b,c,d,e}. --- Attacks: {(a, b), (b, a), (b, c), (c, d), (d, e), (e, c)} --- --- [complete:] --- --- The complete labellings of the argumentation framework 'exampleAF3' --- and 'exampleAF4': --- --- >>> complete exampleAF3 --- [ --- [("A",Undecided),("B",In),("C",Out),("D",In)] --- ] --- --- >>> complete exampleAF4 --- [ --- [("A",Out),("B",In),("C",Out),("D",In),("E",Out)], --- [("A",In),("B",Out),("C",Undecided),("D",Undecided),("E",Undecided)], --- [("A",Out),("B",In),("C",Out),("D",Undecided),("E",Undecided)] --- ] --- --- [completeExt:] --- --- The complete extensions of the argumentation frameworks 'exampleAF3' --- and 'exampleAF4': --- --- >>> completeExt exampleAF3 --- [ --- ["B","D"] --- ] --- >>> completeExt exampleAF4 --- [ --- ["B","D"], --- ["A"], --- ["B"] --- ] --- --- [semiStable:] --- --- The semi-stable labellings of the argumentation framework 'exampleAF3' --- and 'exampleAF4': --- --- >>> semiStable exampleAF3 --- [ --- [("A",Undecided),("B",In),("C",Out),("D",In)] --- ] --- --- >>> semiStable exampleAF4 --- [ --- [("A",Out),("B",In),("C",Out),("D",In),("E",Out)], --- ] --- --- [semiStableExt:] --- --- The complete extensions of the argumentation frameworks 'exampleAF3' --- and 'exampleAF4': --- --- >>> semiStableExt exampleAF3 --- [ --- ["B","D"] --- ] --- >>> semiStableExt exampleAF4 --- [ --- ["B","D"], --- ] --- -exampleAF4 :: DungAF AbsArg -exampleAF4 = AF [a, b, c, d, e] [(a, b), (b, a), (b, c), (c, d), (d, e), (e, c)] - --- |Parsed example as given on the CEGARTIX webpage: --- . --- --- @ --- arg(a). --- arg(b). --- arg(c). --- arg(d). --- arg(e). --- arg(f). --- arg(g). --- att(a,b). --- att(c,b). --- att(c,d). --- att(d,c). --- att(d,e). --- att(e,g). --- att(f,e). --- att(g,f). --- @ --- --- This is given as a literal string to 'parseAF'. -exampleAF5 :: DungAF AbsArg -exampleAF5 = case - parseAF - "arg(a).\ - \arg(b).\ - \arg(c).\ - \arg(d).\ - \arg(e).\ - \arg(f).\ - \arg(g).\ - \att(a,b).\ - \att(c,b).\ - \att(c,d).\ - \att(d,c).\ - \att(d,e).\ - \att(e,g).\ - \att(f,e).\ - \att(g,f)." - of - Left err -> error (show err) - Right af -> af - --- |Output 'String' corresponding to 'exampleAF', --- i.e. @toCegartix exampleAF@. --- --- >>> putStr output --- arg("A"). --- arg("B"). --- arg("C"). --- att("A","B"). --- att("B","C"). -output :: String -output = toCegartix exampleAF - --- |Output 'String' corresponding to 'exampleAF2', --- i.e. @toCegartix exampleAF2@. --- --- >>> putStr output2 --- arg("A"). --- arg("B"). --- att("A","B"). --- att("B","A"). -output2 :: String -output2 = toCegartix exampleAF2 - --- |Output 'String' corresponding to 'exampleAF3', --- i.e. @toCegartix exampleAF3@. --- --- >>> putStr output3 --- arg("A"). --- arg("B"). --- arg("C"). --- arg("D"). --- att("A","A"). --- att("A","C"). --- att("B","C"). --- att("C","D"). -output3 :: String -output3 = toCegartix exampleAF3 - --- |Output 'String' corresponding to 'exampleAF4', --- i.e. @toCegartix exampleAF4@. --- --- >>> putStr output4 --- arg("A"). --- arg("B"). --- arg("C"). --- arg("D"). --- arg("E"). --- att("A","B"). --- att("B","A"). --- att("B","C"). --- att("C","D"). --- att("D","E"). --- att("E","C"). -output4 :: String -output4 = toCegartix exampleAF4 - --- |Output 'String' corresponding to 'exampleAF5', --- i.e. @toCegartix exampleAF5@. -output5 :: String -output5 = toCegartix exampleAF5 - +-- | This is the examples module accompanying the implementation of Dung's +-- argumentation frameworks. +-- +-- This module contains a collection of examples, showing how to define +-- arguments, argumentation frameworks and how to use the standard definitions. +-- +-- To run these examples, or your own: start GHCi and do the following: +-- +-- @\:l Language.Dung.Examples@ +-- +module Language.Dung.Examples + ( + -- * Example uses of the basic definitions + -- |Given @a = \"A\"@, @b = \"B\"@, @c = \"C\"@ + AbsArg, a, b, c, exampleAF, exampleAF2, + -- * Example uses of the fixpoint definitions + faf, + -- * Example uses of the basic labelling definitions + -- |Given @d = \"D\"@, @e = \"E\"@ + d, e, exampleAF3, exampleAF4, + -- * Example uses of the input functionality + exampleAF5, + -- * Example uses of the output functionality + output, output2, output3, output4, output5 + ) + where +import Language.Dung.AF +import Language.Dung.Input +import Language.Dung.Output + +-- $setup +-- >>> :{ +-- >>> let printList :: Show a => [a] -> IO () +-- >>> printList [] = putStrLn "[]" +-- >>> printList [x] = do { putStrLn "[" ; putStrLn (" " ++ show x) ; putStrLn "]" } +-- >>> printList xs = do { putStrLn "[" ; mapM_ (\x -> putStrLn (" " ++ show x ++ ",")) (init xs) ; putStrLn (" " ++ show (last xs)) ; putStrLn "]" } +-- >>> :} + +-- | The simplest abstract argument is an argument identifiable by its name +type AbsArg = String + + +a, b, c :: AbsArg +a = "A" +b = "B" +c = "C" + +-- |Example AF: A -> B -> C +exampleAF :: DungAF AbsArg +exampleAF = AF [a, b, c] [(a, b), (b, c)] + +-- |Example AF: A \<-> B +-- +-- Now follow a few example outputs using the above argumentation frameworks. +-- +-- [setAttacks:] +-- +-- @[a,b]@ 'setAttacks' @c@ in the argumentation framework 'exampleAF': +-- +-- >>> setAttacks exampleAF [a,b] c +-- True +-- +-- >>> setAttacks exampleAF [b,c] a +-- False +-- +-- >>> setAttacks exampleAF2 [] b +-- False +-- +-- [conflictFree:] +-- +-- @\[a,c\]@ is 'conflictFree' in the argumentation framework 'exampleAF': +-- +-- >>> conflictFree exampleAF [a,c] +-- True +-- +-- >>> conflictFree exampleAF [a,b,c] +-- False +-- +-- >>> conflictFree exampleAF2 [a,b] +-- False +-- +-- [acceptable:] +-- +-- @c@ is acceptable w.r.t. @\[a,b\]@ in the argumentation framework 'exampleAF': +-- +-- >>> acceptable exampleAF c [a,b] +-- True +-- +-- >>> acceptable exampleAF c [] +-- False +-- +-- >>> acceptable exampleAF b [a,b,c] +-- False +-- +-- [admissible:] +-- +-- @\[a,b,c\]@ is admissible in the argumentation framework 'exampleAF': +-- +-- >>> admissible exampleAF [a,b,c] +-- False +-- +-- >>> admissible exampleAF [a,c] +-- True +-- +-- >>> admissible exampleAF [a] +-- True +-- +-- [grounded:] +-- +-- The grounded labelling of the argumentation frameworks 'exampleAF' +-- and 'exampleAF2': +-- +-- >>> grounded exampleAF +-- [("A",In),("C",In),("B",Out)] +-- +-- >>> grounded exampleAF2 +-- [("A",Undecided),("B",Undecided)] +-- +-- [groundedExt:] +-- +-- The grounded extension of the argumentation frameworks 'exampleAF' +-- and 'exampleAF2': +-- +-- >>> groundedExt exampleAF +-- ["A","C"] +-- >>> groundedExt exampleAF2 +-- [] +exampleAF2 :: DungAF AbsArg +exampleAF2 = AF [a, b] [(a, b), (b, a)] + +-- |fixed point function for a specific argumentation framework, +-- @faf = f exampleAF@. +-- +-- [groundedF:] +-- +-- The grounded extension of the argumentation framework 'exampleAF' using the +-- fixpoint definition: +-- +-- >>> groundedF faf +-- ["A","C"] +-- +-- >>> groundedF (f exampleAF2) +-- [] +faf :: [AbsArg] -> [AbsArg] +faf = f exampleAF + +d, e :: AbsArg +d = "D" +e = "E" + +-- |Left hand side of Fig1. in Caminada. +-- Arguments are: {a,b,c,d}. +-- Attacks: {(a, a), (a, c), (b, c), (c, d)} +exampleAF3 :: DungAF AbsArg +exampleAF3 = AF [a, b, c, d] [(a, a), (a, c), (b, c), (c, d)] + +-- |Right hand side of Fig1. in Caminada. +-- Arguments are: {a,b,c,d,e}. +-- Attacks: {(a, b), (b, a), (b, c), (c, d), (d, e), (e, c)} +-- +-- [complete:] +-- +-- The complete labellings of the argumentation framework 'exampleAF3' +-- and 'exampleAF4': +-- +-- >>> printList (complete exampleAF3) +-- [ +-- [("A",Undecided),("B",In),("C",Out),("D",In)] +-- ] +-- +-- >>> printList (complete exampleAF4) +-- [ +-- [("A",Out),("B",In),("C",Out),("D",In),("E",Out)], +-- [("A",In),("B",Out),("C",Undecided),("D",Undecided),("E",Undecided)], +-- [("A",Out),("B",In),("C",Out),("D",Undecided),("E",Undecided)] +-- ] +-- +-- [completeExt:] +-- +-- The complete extensions of the argumentation frameworks 'exampleAF3' +-- and 'exampleAF4': +-- +-- >>> printList (completeExt exampleAF3) +-- [ +-- ["B","D"] +-- ] +-- >>> printList (completeExt exampleAF4) +-- [ +-- ["B","D"], +-- ["A"], +-- ["B"] +-- ] +-- +-- [semiStable:] +-- +-- The semi-stable labellings of the argumentation framework 'exampleAF3' +-- and 'exampleAF4': +-- +-- >>> printList (semiStable exampleAF3) +-- [ +-- [("A",Undecided),("B",In),("C",Out),("D",In)] +-- ] +-- +-- >>> printList (semiStable exampleAF4) +-- [ +-- [("A",Out),("B",In),("C",Out),("D",In),("E",Out)] +-- ] +-- +-- [semiStableExt:] +-- +-- The complete extensions of the argumentation frameworks 'exampleAF3' +-- and 'exampleAF4': +-- +-- >>> printList (semiStableExt exampleAF3) +-- [ +-- ["B","D"] +-- ] +-- >>> printList (semiStableExt exampleAF4) +-- [ +-- ["B","D"] +-- ] +-- +exampleAF4 :: DungAF AbsArg +exampleAF4 = AF [a, b, c, d, e] [(a, b), (b, a), (b, c), (c, d), (d, e), (e, c)] + +-- |Parsed example as given on the CEGARTIX webpage: +-- . +-- +-- @ +-- arg(a). +-- arg(b). +-- arg(c). +-- arg(d). +-- arg(e). +-- arg(f). +-- arg(g). +-- att(a,b). +-- att(c,b). +-- att(c,d). +-- att(d,c). +-- att(d,e). +-- att(e,g). +-- att(f,e). +-- att(g,f). +-- @ +-- +-- This is given as a literal string to 'parseAF'. +exampleAF5 :: DungAF AbsArg +exampleAF5 = case + parseAF + "arg(a).\ + \arg(b).\ + \arg(c).\ + \arg(d).\ + \arg(e).\ + \arg(f).\ + \arg(g).\ + \att(a,b).\ + \att(c,b).\ + \att(c,d).\ + \att(d,c).\ + \att(d,e).\ + \att(e,g).\ + \att(f,e).\ + \att(g,f)." + of + Left err -> error (show err) + Right af -> af + +-- |Output 'String' corresponding to 'exampleAF', +-- i.e. @toCegartix exampleAF@. +-- +-- >>> putStr output +-- arg("A"). +-- arg("B"). +-- arg("C"). +-- att("A","B"). +-- att("B","C"). +output :: String +output = toCegartix exampleAF + +-- |Output 'String' corresponding to 'exampleAF2', +-- i.e. @toCegartix exampleAF2@. +-- +-- >>> putStr output2 +-- arg("A"). +-- arg("B"). +-- att("A","B"). +-- att("B","A"). +output2 :: String +output2 = toCegartix exampleAF2 + +-- |Output 'String' corresponding to 'exampleAF3', +-- i.e. @toCegartix exampleAF3@. +-- +-- >>> putStr output3 +-- arg("A"). +-- arg("B"). +-- arg("C"). +-- arg("D"). +-- att("A","A"). +-- att("A","C"). +-- att("B","C"). +-- att("C","D"). +output3 :: String +output3 = toCegartix exampleAF3 + +-- |Output 'String' corresponding to 'exampleAF4', +-- i.e. @toCegartix exampleAF4@. +-- +-- >>> putStr output4 +-- arg("A"). +-- arg("B"). +-- arg("C"). +-- arg("D"). +-- arg("E"). +-- att("A","B"). +-- att("B","A"). +-- att("B","C"). +-- att("C","D"). +-- att("D","E"). +-- att("E","C"). +output4 :: String +output4 = toCegartix exampleAF4 + +-- |Output 'String' corresponding to 'exampleAF5', +-- i.e. @toCegartix exampleAF5@. +output5 :: String +output5 = toCegartix exampleAF5 + diff --git a/src/Language/Dung/Input.hs b/src/Language/Dung/Input.hs --- a/src/Language/Dung/Input.hs +++ b/src/Language/Dung/Input.hs @@ -1,90 +1,88 @@ --- | This is the input module accompanying the implementation of Dung's --- argumentation frameworks. It defines a simple parser for an argumentation framework --- that assumes the input file is in CEGARTIX/PrefSat-like format. --- --- Files are assumed to have one argument or attack on each line, ending --- in a dot. (Our parser is slightly more relaxed than this and doesn't care about whitespace.) --- --- @att(a1,a2).@ or @arg(a1).@ --- --- Argument names are assumed to consist only of letters and numbers. --- Arguments used in attacks should be declared separately as well. - -module Language.Dung.Input - ( - -- * Parsing functions - parseAF, pAF - ) - where -import Language.Dung.AF -import Text.Parsec -import Text.Parsec.String (Parser) -import Text.Parsec.Char (char, string) -import qualified Text.Parsec.Token as P -import Text.Parsec.Language(haskellStyle) -import Text.Parsec.Error(errorMessages, messageString) -import Data.Either (partitionEithers) - -lexer :: P.TokenParser () -lexer = P.makeTokenParser haskellStyle - -whiteSpace :: Parser () -whiteSpace = P.whiteSpace lexer - -identifier :: Parser String -identifier = P.identifier lexer - -stringLiteral :: Parser String -stringLiteral = P.stringLiteral lexer - --- |An argument name consists of one or more letters and digits --- or a string literal. -argName :: Parser String -argName = try identifier <|> stringLiteral - --- |A complete argument consists of @arg(argName).@ -pArgument :: Parser String -pArgument = do - string "arg(" - arg <- argName - string ")." - whiteSpace - return arg - --- |A complete attack consists of @atk(argName,argName).@ --- or @att(argName,argName).@. -pAttack :: Parser (String, String) -pAttack = do - string "at" - string "t(" <|> string "k(" - arg1 <- argName - char ',' - whiteSpace - arg2 <- argName - string ")." - return (arg1, arg2) - --- |Parses one attack or argument and returns the result --- in the 'Either' data type. -pArgOrAttack :: Parser (Either String (String, String)) -pArgOrAttack = try (do arg <- pArgument - whiteSpace - return $ Left arg) - <|> - do atk <- pAttack - whiteSpace - return $ Right atk - --- |An AF is parsed by parsing at least one argument or attack, --- followed by an end of file token. -pAF :: Parser (DungAF String) -pAF = do - ps <- many1 pArgOrAttack - eof - let (args, atks) = partitionEithers ps - return $ AF args atks - --- |Parses a 'String' containing multiple arguments/attacks. --- If parsing fails, it propagates the parse error. -parseAF :: String -> Either ParseError (DungAF String) +-- | This is the input module accompanying the implementation of Dung's +-- argumentation frameworks. It defines a simple parser for an argumentation framework +-- that assumes the input file is in CEGARTIX/PrefSat-like format. +-- +-- Files are assumed to have one argument or attack on each line, ending +-- in a dot. (Our parser is slightly more relaxed than this and doesn't care about whitespace.) +-- +-- @att(a1,a2).@ or @arg(a1).@ +-- +-- Argument names are assumed to consist only of letters and numbers. +-- Arguments used in attacks should be declared separately as well. + +module Language.Dung.Input + ( + -- * Parsing functions + parseAF, pAF + ) + where +import Language.Dung.AF +import Text.Parsec +import Text.Parsec.String (Parser) +import qualified Text.Parsec.Token as P +import Text.Parsec.Language (haskellStyle) +import Data.Either (partitionEithers) + +lexer :: P.TokenParser () +lexer = P.makeTokenParser haskellStyle + +whiteSpace :: Parser () +whiteSpace = P.whiteSpace lexer + +identifier :: Parser String +identifier = P.identifier lexer + +stringLiteral :: Parser String +stringLiteral = P.stringLiteral lexer + +-- |An argument name consists of one or more letters and digits +-- or a string literal. +argName :: Parser String +argName = try identifier <|> stringLiteral + +-- |A complete argument consists of @arg(argName).@ +pArgument :: Parser String +pArgument = do + _ <- string "arg(" + arg <- argName + _ <- string ")." + whiteSpace + return arg + +-- |A complete attack consists of @atk(argName,argName).@ +-- or @att(argName,argName).@. +pAttack :: Parser (String, String) +pAttack = do + _ <- string "at" + _ <- string "t(" <|> string "k(" + arg1 <- argName + _ <- char ',' + whiteSpace + arg2 <- argName + _ <- string ")." + return (arg1, arg2) + +-- |Parses one attack or argument and returns the result +-- in the 'Either' data type. +pArgOrAttack :: Parser (Either String (String, String)) +pArgOrAttack = try (do arg <- pArgument + whiteSpace + return $ Left arg) + <|> + do atk <- pAttack + whiteSpace + return $ Right atk + +-- |An AF is parsed by parsing at least one argument or attack, +-- followed by an end of file token. +pAF :: Parser (DungAF String) +pAF = do + ps <- many1 pArgOrAttack + eof + let (args, atks) = partitionEithers ps + return $ AF args atks + +-- |Parses a 'String' containing multiple arguments/attacks. +-- If parsing fails, it propagates the parse error. +parseAF :: String -> Either ParseError (DungAF String) parseAF = parse pAF "" diff --git a/src/Language/Dung/Output.hs b/src/Language/Dung/Output.hs --- a/src/Language/Dung/Output.hs +++ b/src/Language/Dung/Output.hs @@ -1,60 +1,60 @@ --- | This is the output module accompanying the implementation of Dung's --- argumentation frameworks. It allows an implemented argumentation framework --- to be outputted to files in a standard format. --- --- This module currently contains two output format. The strict version is readable --- by both CEGARTIX and PrefSat. The lax version keeps more of the original formatting. -module Language.Dung.Output - ( - -- * CEGARTIX/PrefSat output - argToCegartix, atkToCegartix, toCegartix, - argToStrictCegartix, atkToStrictCegartix, toStrictCegartix - ) - where -import Language.Dung.AF - - --- |Converts an argument to a CEGARTIX 'String'. All argument names are made --- into string literals removing extra quotes. Additionally all parentheses are removed. -argToStrictCegartix :: Show arg => arg -> String -argToStrictCegartix arg = "arg(" ++ (show . remParens . remQuote . show) arg ++ ").\n" - --- |Converts an attack to a CEGARTIX 'String'. All argument names are made --- into string literals removing extra quotes. Additionally all parentheses are removed. -atkToStrictCegartix :: Show arg => (arg, arg) -> String -atkToStrictCegartix (a,b) = "att(" ++ (show . remParens . remQuote . show) a ++ "," ++ (show . remQuote. show) b ++ ").\n" - --- |Converts an argument to a CEGARTIX 'String'. All argument names are made --- into string literals removing extra quotes. -argToCegartix :: Show arg => arg -> String -argToCegartix arg = "arg(" ++ (show . remQuote . show) arg ++ ").\n" - --- |Converts an attack to a CEGARTIX 'String'. All argument names are made --- into string literals removing extra quotes. -atkToCegartix :: Show arg => (arg, arg) -> String -atkToCegartix (a,b) = "att(" ++ (show . remQuote . show) a ++ "," ++ (show . remQuote. show) b ++ ").\n" - --- |Outputs an argumentation frameworks in CEGARTIX/PrefSat format. -toCegartix :: Show arg => DungAF arg -> String -toCegartix (AF args att) = - concatMap argToCegartix args - ++ concatMap atkToCegartix att - --- |Outputs an argumentation frameworks in strict CEGARTIX/PrefSat format. -toStrictCegartix :: Show arg => DungAF arg -> String -toStrictCegartix (AF args att) = - concatMap argToStrictCegartix args - ++ concatMap atkToStrictCegartix att - --- toCegartix :: Show arg => DungAF arg -> IO () --- toCegartix (AF args att) = do - -- mapM_ (putStr . argToCegartix) args - -- mapM_ (putStr . atkToCegartix) att - --- |Remove all quotes from a 'String'. -remQuote :: String -> String -remQuote = filter (/= '"') - --- |Remove all parentheses from a 'String'. -remParens :: String -> String +-- | This is the output module accompanying the implementation of Dung's +-- argumentation frameworks. It allows an implemented argumentation framework +-- to be outputted to files in a standard format. +-- +-- This module currently contains two output format. The strict version is readable +-- by both CEGARTIX and PrefSat. The lax version keeps more of the original formatting. +module Language.Dung.Output + ( + -- * CEGARTIX/PrefSat output + argToCegartix, atkToCegartix, toCegartix, + argToStrictCegartix, atkToStrictCegartix, toStrictCegartix + ) + where +import Language.Dung.AF + + +-- |Converts an argument to a CEGARTIX 'String'. All argument names are made +-- into string literals removing extra quotes. Additionally all parentheses are removed. +argToStrictCegartix :: Show arg => arg -> String +argToStrictCegartix arg = "arg(" ++ (show . remParens . remQuote . show) arg ++ ").\n" + +-- |Converts an attack to a CEGARTIX 'String'. All argument names are made +-- into string literals removing extra quotes. Additionally all parentheses are removed. +atkToStrictCegartix :: Show arg => (arg, arg) -> String +atkToStrictCegartix (a,b) = "att(" ++ (show . remParens . remQuote . show) a ++ "," ++ (show . remQuote. show) b ++ ").\n" + +-- |Converts an argument to a CEGARTIX 'String'. All argument names are made +-- into string literals removing extra quotes. +argToCegartix :: Show arg => arg -> String +argToCegartix arg = "arg(" ++ (show . remQuote . show) arg ++ ").\n" + +-- |Converts an attack to a CEGARTIX 'String'. All argument names are made +-- into string literals removing extra quotes. +atkToCegartix :: Show arg => (arg, arg) -> String +atkToCegartix (a,b) = "att(" ++ (show . remQuote . show) a ++ "," ++ (show . remQuote. show) b ++ ").\n" + +-- |Outputs an argumentation frameworks in CEGARTIX/PrefSat format. +toCegartix :: Show arg => DungAF arg -> String +toCegartix (AF args att) = + concatMap argToCegartix args + ++ concatMap atkToCegartix att + +-- |Outputs an argumentation frameworks in strict CEGARTIX/PrefSat format. +toStrictCegartix :: Show arg => DungAF arg -> String +toStrictCegartix (AF args att) = + concatMap argToStrictCegartix args + ++ concatMap atkToStrictCegartix att + +-- toCegartix :: Show arg => DungAF arg -> IO () +-- toCegartix (AF args att) = do + -- mapM_ (putStr . argToCegartix) args + -- mapM_ (putStr . atkToCegartix) att + +-- |Remove all quotes from a 'String'. +remQuote :: String -> String +remQuote = filter (/= '"') + +-- |Remove all parentheses from a 'String'. +remParens :: String -> String remParens = filter (\ x -> x /= '(' && x /= ')') diff --git a/src/Main.hs b/src/Main.hs deleted file mode 100644 --- a/src/Main.hs +++ /dev/null @@ -1,97 +0,0 @@ --- |This module implements a command-line interface to the implementation of --- Dung's argumentation frameworks. Dung + Haskell = Dungell --- --- Code in this module partly taken from/inspired by Shinobu --- See: http://zuttobenkyou.wordpress.com/2011/04/19/haskell-using-cmdargs-single-and-multi-mode/ --- and http://listx.github.com/ -{-# LANGUAGE DeriveDataTypeable, RecordWildCards #-} -module Main - ( - main - ) - where -import Language.Dung.AF(groundedExt, preferredExt, stableExt, semiStableExt, - DungAF(..)) -import Language.Dung.Input -import Language.Dung.Output - -import System.Console.CmdArgs -import System.Environment (getArgs, withArgs) -import System.Exit -import Control.Monad (when, unless) - -data MyOptions = MyOptions { - cegartix :: Bool, - laxCegartix :: Bool, - fileName :: String, - outputFile :: String, - grounded :: Bool, - preferred :: Bool, - stable :: Bool, - semiStable :: Bool, - all :: Bool - } deriving (Show, Data, Typeable) - -myProgOpts :: MyOptions -myProgOpts = MyOptions - { cegartix = True &= help "Output in strict CEGARTIX/PrefSat format (standard)" - , laxCegartix = False &= help "Output in lax CEGARTIX/PrefSat format (+parentheses)" - , fileName = def &= typFile &= help "Name of the file to be read" - , outputFile = def &= typFile &= help "Name of the file to be written" - , grounded = False &= help "Output grounded extension for the AF" - , preferred = False &= help "Output preferred extensions for the AF" - , stable = False &= help "Output stable extensions for the AF" - , semiStable = False &= help "Output semi-stable extensions for the AF" - , all = False &= help "Output extensions of all implemented semantics for AF" - } - -getOpts :: IO MyOptions -getOpts = cmdArgs $ myProgOpts - -- &= verbosityArgs [explicit, name "Verbose", name "V"] [] - &= versionArg [explicit, name "version", name "v", summary _PROGRAM_INFO] - &= summary (_PROGRAM_INFO ++ ", " ++ _COPYRIGHT) - &= help _PROGRAM_ABOUT - &= helpArg [explicit, name "help", name "h"] - &= program _PROGRAM_NAME - -_PROGRAM_NAME = "Dungell" -_PROGRAM_VERSION = "1.0.0.1" -_PROGRAM_INFO = _PROGRAM_NAME ++ " version " ++ _PROGRAM_VERSION -_PROGRAM_ABOUT = "An implementation of Dung's AFs" -_COPYRIGHT = "(C) Bas van Gijzel 2014" - - -main :: IO () -main = do - args <- getArgs - opts <- (if null args then withArgs ["--help"] else id) getOpts - optionHandler opts - --- |Check any malformed arguments/missing arguments. -optionHandler :: MyOptions -> IO () -optionHandler opts@MyOptions{..} = do - when (null fileName) $ putStrLn "--fileName is blank!" >> exitWith (ExitFailure 1) - input <- readFile fileName - let opts' = opts {cegartix = not laxCegartix} - af <- case parseAF input of - Left err -> putStrLn "Parsing error: " >> print err >> exitWith (ExitFailure 1) - Right af -> return af - let opts'' = if all - then - opts' {grounded = True, preferred = True, stable = True, semiStable = True} - else - opts' - exec opts'' af - --- |Execute supplied options -exec :: (Show arg, Eq arg, Ord arg) => MyOptions -> DungAF arg -> IO () -exec opts@MyOptions{..} af = do - print af - when grounded $ putStr "grounded: " >> print (groundedExt af) - when preferred $ putStr "preferred: " >> print (preferredExt af) - when stable $ putStr "stable: " >> print (stableExt af) - when semiStable $ putStr "semi-stable: " >> print (semiStableExt af) - unless (null outputFile) - $ if cegartix - then writeFile outputFile (toStrictCegartix af) >> putStrLn "File outputted." - else writeFile outputFile (toCegartix af) >> putStrLn "File outputted." diff --git a/test/Doctest.hs b/test/Doctest.hs new file mode 100644 --- /dev/null +++ b/test/Doctest.hs @@ -0,0 +1,11 @@ +module Main (main) where + +import Test.DocTest + +main :: IO () +main = doctest + [ "-isrc" + , "-package", "containers" + , "-package", "parsec" + , "src/Language/Dung/Examples.hs" + ] diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,14 @@ +module Main (main) where + +import Test.Tasty + +import qualified Test.Language.Dung.AF as AF +import qualified Test.Language.Dung.Input as Input +import qualified Test.Language.Dung.Properties as Properties + +main :: IO () +main = defaultMain $ testGroup "Dung" + [ AF.tests + , Input.tests + , Properties.tests + ] diff --git a/test/Test/Language/Dung/AF.hs b/test/Test/Language/Dung/AF.hs new file mode 100644 --- /dev/null +++ b/test/Test/Language/Dung/AF.hs @@ -0,0 +1,184 @@ +module Test.Language.Dung.AF (tests) where + +import Data.List (sort) +import Test.Tasty +import Test.Tasty.HUnit + +import Language.Dung.AF + +-- Convenience definitions matching Examples.hs +a, b, c, d, e :: String +a = "A" +b = "B" +c = "C" +d = "D" +e = "E" + +-- A -> B -> C +exampleAF :: DungAF String +exampleAF = AF [a, b, c] [(a, b), (b, c)] + +-- A <-> B +exampleAF2 :: DungAF String +exampleAF2 = AF [a, b] [(a, b), (b, a)] + +-- Fig1 LHS in Caminada: {(a,a), (a,c), (b,c), (c,d)} +exampleAF3 :: DungAF String +exampleAF3 = AF [a, b, c, d] [(a, a), (a, c), (b, c), (c, d)] + +-- Fig1 RHS in Caminada: {(a,b), (b,a), (b,c), (c,d), (d,e), (e,c)} +exampleAF4 :: DungAF String +exampleAF4 = AF [a, b, c, d, e] [(a, b), (b, a), (b, c), (c, d), (d, e), (e, c)] + +tests :: TestTree +tests = testGroup "Language.Dung.AF" + [ setAttacksTests + , conflictFreeTests + , acceptableTests + , admissibleTests + , groundedTests + , groundedExtTests + , groundedFTests + , completeTests + , completeExtTests + , preferredExtTests + , stableExtTests + , semiStableTests + , semiStableExtTests + ] + +setAttacksTests :: TestTree +setAttacksTests = testGroup "setAttacks" + [ testCase "[a,b] attacks c in exampleAF" $ + setAttacks exampleAF [a, b] c @?= True + , testCase "[b,c] does not attack a in exampleAF" $ + setAttacks exampleAF [b, c] a @?= False + , testCase "[] does not attack b in exampleAF2" $ + setAttacks exampleAF2 [] b @?= False + ] + +conflictFreeTests :: TestTree +conflictFreeTests = testGroup "conflictFree" + [ testCase "[a,c] is conflict-free in exampleAF" $ + conflictFree exampleAF [a, c] @?= True + , testCase "[a,b,c] is not conflict-free in exampleAF" $ + conflictFree exampleAF [a, b, c] @?= False + , testCase "[a,b] is not conflict-free in exampleAF2" $ + conflictFree exampleAF2 [a, b] @?= False + ] + +acceptableTests :: TestTree +acceptableTests = testGroup "acceptable" + [ testCase "c acceptable w.r.t. [a,b] in exampleAF" $ + acceptable exampleAF c [a, b] @?= True + , testCase "c not acceptable w.r.t. [] in exampleAF" $ + acceptable exampleAF c [] @?= False + , testCase "b not acceptable w.r.t. [a,b,c] in exampleAF" $ + acceptable exampleAF b [a, b, c] @?= False + ] + +admissibleTests :: TestTree +admissibleTests = testGroup "admissible" + [ testCase "[a,b,c] not admissible in exampleAF" $ + admissible exampleAF [a, b, c] @?= False + , testCase "[a,c] is admissible in exampleAF" $ + admissible exampleAF [a, c] @?= True + , testCase "[a] is admissible in exampleAF" $ + admissible exampleAF [a] @?= True + ] + +groundedTests :: TestTree +groundedTests = testGroup "grounded" + [ testCase "grounded exampleAF" $ + sort (grounded exampleAF) @?= sort [("A", In), ("C", In), ("B", Out)] + , testCase "grounded exampleAF2" $ + sort (grounded exampleAF2) @?= sort [("A", Undecided), ("B", Undecided)] + ] + +groundedExtTests :: TestTree +groundedExtTests = testGroup "groundedExt" + [ testCase "groundedExt exampleAF" $ + sort (groundedExt exampleAF) @?= sort ["A", "C"] + , testCase "groundedExt exampleAF2" $ + groundedExt exampleAF2 @?= [] + ] + +groundedFTests :: TestTree +groundedFTests = testGroup "groundedF" + [ testCase "groundedF (f exampleAF)" $ + sort (groundedF (f exampleAF)) @?= sort ["A", "C"] + , testCase "groundedF (f exampleAF2)" $ + groundedF (f exampleAF2) @?= [] + , testCase "groundedF' (f exampleAF)" $ + sort (groundedF' (f exampleAF)) @?= sort ["A", "C"] + , testCase "groundedF' (f exampleAF2)" $ + groundedF' (f exampleAF2) @?= [] + ] + +completeTests :: TestTree +completeTests = testGroup "complete" + [ testCase "complete exampleAF3 has one labelling" $ + length (complete exampleAF3) @?= 1 + , testCase "complete exampleAF3 content" $ case complete exampleAF3 of + (lab:_) -> sort lab @?= sort [("A", Undecided), ("B", In), ("C", Out), ("D", In)] + [] -> assertFailure "Expected at least one complete labelling" + , testCase "complete exampleAF4 has three labellings" $ + length (complete exampleAF4) @?= 3 + ] + +completeExtTests :: TestTree +completeExtTests = testGroup "completeExt" + [ testCase "completeExt exampleAF3" $ + map sort (completeExt exampleAF3) @?= [sort ["B", "D"]] + , testCase "completeExt exampleAF4 has three extensions" $ + length (completeExt exampleAF4) @?= 3 + , testCase "completeExt exampleAF4 content" $ do + let exts = map sort (completeExt exampleAF4) + sort ["B", "D"] `elem` exts @?= True + sort ["A"] `elem` exts @?= True + sort ["B"] `elem` exts @?= True + ] + +preferredExtTests :: TestTree +preferredExtTests = testGroup "preferredExt" + [ testCase "preferredExt exampleAF" $ + map sort (preferredExt exampleAF) @?= [sort ["A", "C"]] + , testCase "preferredExt exampleAF2" $ do + let exts = map sort (preferredExt exampleAF2) + length exts @?= 2 + ["A"] `elem` exts @?= True + ["B"] `elem` exts @?= True + ] + +stableExtTests :: TestTree +stableExtTests = testGroup "stableExt" + [ testCase "stableExt exampleAF" $ + map sort (stableExt exampleAF) @?= [sort ["A", "C"]] + , testCase "stableExt exampleAF2" $ do + let exts = map sort (stableExt exampleAF2) + length exts @?= 2 + ["A"] `elem` exts @?= True + ["B"] `elem` exts @?= True + ] + +semiStableTests :: TestTree +semiStableTests = testGroup "semiStable" + [ testCase "semiStable exampleAF3 has one labelling" $ + length (semiStable exampleAF3) @?= 1 + , testCase "semiStable exampleAF3 content" $ case semiStable exampleAF3 of + (s:_) -> sort s @?= sort [("A", Undecided), ("B", In), ("C", Out), ("D", In)] + [] -> assertFailure "Expected at least one semi-stable labelling" + , testCase "semiStable exampleAF4 has one labelling" $ + length (semiStable exampleAF4) @?= 1 + , testCase "semiStable exampleAF4 content" $ case semiStable exampleAF4 of + (s:_) -> sort s @?= sort [("A", Out), ("B", In), ("C", Out), ("D", In), ("E", Out)] + [] -> assertFailure "Expected at least one semi-stable labelling" + ] + +semiStableExtTests :: TestTree +semiStableExtTests = testGroup "semiStableExt" + [ testCase "semiStableExt exampleAF3" $ + map sort (semiStableExt exampleAF3) @?= [sort ["B", "D"]] + , testCase "semiStableExt exampleAF4" $ + map sort (semiStableExt exampleAF4) @?= [sort ["B", "D"]] + ] diff --git a/test/Test/Language/Dung/Input.hs b/test/Test/Language/Dung/Input.hs new file mode 100644 --- /dev/null +++ b/test/Test/Language/Dung/Input.hs @@ -0,0 +1,79 @@ +module Test.Language.Dung.Input (tests) where + +import Test.Tasty +import Test.Tasty.HUnit + +import Language.Dung.AF +import Language.Dung.Input +import Language.Dung.Output + +tests :: TestTree +tests = testGroup "Language.Dung.Input" + [ parseTests + , roundTripTests + , edgeCaseTests + ] + +-- Helper to unwrap a Right or fail the test +expectRight :: Show a => Either a b -> IO b +expectRight (Right x) = return x +expectRight (Left err) = assertFailure ("Expected Right but got Left: " ++ show err) + +parseTests :: TestTree +parseTests = testGroup "parseAF" + [ testCase "parses single argument" $ do + af <- expectRight $ parseAF "arg(a)." + af @?= AF ["a"] [] + , testCase "parses argument and attack" $ do + af <- expectRight $ parseAF "arg(a). arg(b). att(a,b)." + af @?= AF ["a", "b"] [("a", "b")] + , testCase "parses atk syntax" $ do + af <- expectRight $ parseAF "arg(a). arg(b). atk(a,b)." + af @?= AF ["a", "b"] [("a", "b")] + , testCase "parses multi-line input" $ do + let input = unlines + [ "arg(a)." + , "arg(b)." + , "arg(c)." + , "att(a,b)." + , "att(b,c)." + ] + af <- expectRight $ parseAF input + af @?= AF ["a", "b", "c"] [("a", "b"), ("b", "c")] + , testCase "parses exampleaf.txt format" $ do + let input = "arg(a). arg(b). arg(c). arg(d). arg(e). arg(f). arg(g). att(a,b). att(c,b). att(c,d). att(d,c). att(d,e). att(e,g). att(f,e). att(g,f)." + af <- expectRight $ parseAF input + af @?= AF ["a","b","c","d","e","f","g"] + [("a","b"),("c","b"),("c","d"),("d","c"),("d","e"),("e","g"),("f","e"),("g","f")] + , testCase "returns Left on invalid input" $ do + let result = parseAF "invalid input" + case result of + Left _ -> return () + Right _ -> assertFailure "Expected parse error" + ] + +roundTripTests :: TestTree +roundTripTests = testGroup "round-trip" + [ testCase "parse . toCegartix identity for simple AF" $ do + let af = AF ["a", "b", "c"] [("a", "b"), ("b", "c")] :: DungAF String + output = toCegartix af + case parseAF output of + Left err -> assertFailure $ "Parse error: " ++ show err + Right af' -> af' @?= af + , testCase "parse . toCegartix identity for self-attacking AF" $ do + let af = AF ["a", "b"] [("a", "a"), ("a", "b")] :: DungAF String + output = toCegartix af + case parseAF output of + Left err -> assertFailure $ "Parse error: " ++ show err + Right af' -> af' @?= af + ] + +edgeCaseTests :: TestTree +edgeCaseTests = testGroup "edge cases" + [ testCase "single argument, no attacks" $ do + af <- expectRight $ parseAF "arg(x)." + af @?= AF ["x"] [] + , testCase "string literal argument names" $ do + af <- expectRight $ parseAF "arg(\"hello\"). arg(\"world\"). att(\"hello\", \"world\")." + af @?= AF ["hello", "world"] [("hello", "world")] + ] diff --git a/test/Test/Language/Dung/Properties.hs b/test/Test/Language/Dung/Properties.hs new file mode 100644 --- /dev/null +++ b/test/Test/Language/Dung/Properties.hs @@ -0,0 +1,81 @@ +module Test.Language.Dung.Properties (tests) where + +import Data.List (sort) +import qualified Data.Set as Set +import Test.Tasty +import Test.Tasty.QuickCheck + +import Language.Dung.AF + +-- Generate small AFs with 3-5 arguments for tractable computation +newtype SmallAF = SmallAF (DungAF String) + deriving (Show) + +instance Arbitrary SmallAF where + arbitrary = do + n <- choose (3, 5 :: Int) + let args = map (\i -> "a" ++ show i) [1..n] + numAtks <- choose (0, n * n `div` 2) + atks <- vectorOf numAtks $ do + from <- elements args + to <- elements args + return (from, to) + -- Remove duplicate attacks + let uniqueAtks = Set.toList . Set.fromList $ atks + return $ SmallAF (AF args uniqueAtks) + +-- Helper: check if a set is a subset of another +isSubsetOf :: Ord a => [a] -> [a] -> Bool +isSubsetOf xs ys = Set.fromList xs `Set.isSubsetOf` Set.fromList ys + +tests :: TestTree +tests = testGroup "QuickCheck Properties" + [ groundedProperties + , preferredProperties + , stableProperties + , semanticRelationProperties + ] + +groundedProperties :: TestTree +groundedProperties = testGroup "grounded" + [ testProperty "grounded extension is conflict-free" $ \(SmallAF af) -> + conflictFree af (groundedExt af) + , testProperty "grounded extension is admissible" $ \(SmallAF af) -> + admissible af (groundedExt af) + , testProperty "grounded labelling covers all arguments" $ \(SmallAF af@(AF args _)) -> + sort (map fst (grounded af)) == sort args + ] + +preferredProperties :: TestTree +preferredProperties = testGroup "preferred" + [ testProperty "every preferred extension is admissible" $ \(SmallAF af) -> + all (admissible af) (preferredExt af) + , testProperty "every preferred extension is conflict-free" $ \(SmallAF af) -> + all (conflictFree af) (preferredExt af) + , testProperty "at least one preferred extension exists" $ \(SmallAF af) -> + not (null (preferredExt af)) + ] + +stableProperties :: TestTree +stableProperties = testGroup "stable" + [ testProperty "every stable extension is also a preferred extension" $ \(SmallAF af) -> + let stExts = map sort (stableExt af) + prExts = map sort (preferredExt af) + in all (`elem` prExts) stExts + , testProperty "every stable extension is conflict-free" $ \(SmallAF af) -> + all (conflictFree af) (stableExt af) + ] + +semanticRelationProperties :: TestTree +semanticRelationProperties = testGroup "semantic relations" + [ testProperty "grounded is the smallest complete extension" $ \(SmallAF af) -> + let gExt = sort (groundedExt af) + cExts = completeExt af + in all (\ce -> gExt `isSubsetOf` ce) cExts + , testProperty "every complete extension is admissible" $ \(SmallAF af) -> + all (admissible af) (completeExt af) + , testProperty "groundedF agrees with groundedExt" $ \(SmallAF af) -> + sort (groundedF (f af)) == sort (groundedExt af) + , testProperty "groundedF' agrees with groundedExt" $ \(SmallAF af) -> + sort (groundedF' (f af)) == sort (groundedExt af) + ]