{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE TemplateHaskell #-}

module Modelling.ActivityDiagram.Alloy(
  adConfigBitWidth,
  adConfigScope,
  adConfigToAlloy,
  adConfigToAlloy', -- only for test cases
  modulePetriNet,
  moduleActionSequencesRules
) where

import Modelling.ActivityDiagram.Config (AdConfig (..))

import Data.FileEmbed                   (embedStringFile)
import Data.String.Interpolate          (i)

moduleComponentsSig :: String
moduleComponentsSig :: String
moduleComponentsSig = Int -> String -> String
removeLines Int
1 $(embedStringFile "alloy/ad/components.als")

moduleInitialNodeRules :: String
moduleInitialNodeRules :: String
moduleInitialNodeRules =
  Int -> String -> String
removeLines Int
3 $(embedStringFile "alloy/ad/initialNodeRules.als")

moduleNameRules :: String
moduleNameRules :: String
moduleNameRules = Int -> String -> String
removeLines Int
3 $(embedStringFile "alloy/ad/nameRules.als")

moduleReachabilityRules :: String
moduleReachabilityRules :: String
moduleReachabilityRules =
  Int -> String -> String
removeLines Int
3 $(embedStringFile "alloy/ad/reachabilityRules.als")

modulePlantUMLSig :: String
modulePlantUMLSig :: String
modulePlantUMLSig = Int -> String -> String
removeLines Int
3 $(embedStringFile "alloy/ad/plantUml.als")

moduleExerciseRules :: String
moduleExerciseRules :: String
moduleExerciseRules =
  Int -> String -> String
removeLines Int
3 $(embedStringFile "alloy/ad/exerciseRules.als")

modulePetriNet :: String
modulePetriNet :: String
modulePetriNet = Int -> String -> String
removeLines Int
3 $(embedStringFile "alloy/ad/petriNet.als")

moduleActionSequencesRules :: String
moduleActionSequencesRules :: String
moduleActionSequencesRules =
  Int -> String -> String
removeLines Int
3 $(embedStringFile "alloy/ad/actionSequencesRules.als")

removeLines :: Int -> String -> String
removeLines :: Int -> String -> String
removeLines Int
n = [String] -> String
unlines ([String] -> String) -> (String -> [String]) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [String] -> [String]
forall a. Int -> [a] -> [a]
drop Int
n ([String] -> [String])
-> (String -> [String]) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines

adConfigToAlloy :: String -> String -> AdConfig -> String
adConfigToAlloy :: String -> String -> AdConfig -> String
adConfigToAlloy String
modules String
predicates AdConfig
adConf = Int -> Int -> String -> String -> AdConfig -> String
adConfigToAlloy'
  (AdConfig -> Int
adConfigScope AdConfig
adConf)
  (AdConfig -> Int
adConfigBitWidth AdConfig
adConf)
  String
modules
  String
predicates
  AdConfig
adConf

adConfigToAlloy' :: Int -> Int -> String -> String -> AdConfig -> String
adConfigToAlloy' :: Int -> Int -> String -> String -> AdConfig -> String
adConfigToAlloy' Int
scope Int
bitWidth String
modules String
predicates AdConfig {
    (Int, Int)
actionLimits :: (Int, Int)
actionLimits :: AdConfig -> (Int, Int)
actionLimits,
    (Int, Int)
objectNodeLimits :: (Int, Int)
objectNodeLimits :: AdConfig -> (Int, Int)
objectNodeLimits,
    Int
maxNamedNodes :: Int
maxNamedNodes :: AdConfig -> Int
maxNamedNodes,
    Int
decisionMergePairs :: Int
decisionMergePairs :: AdConfig -> Int
decisionMergePairs,
    Int
forkJoinPairs :: Int
forkJoinPairs :: AdConfig -> Int
forkJoinPairs,
    Int
activityFinalNodes :: Int
activityFinalNodes :: AdConfig -> Int
activityFinalNodes,
    Int
flowFinalNodes :: Int
flowFinalNodes :: AdConfig -> Int
flowFinalNodes,
    Int
cycles :: Int
cycles :: AdConfig -> Int
cycles
  } =
  [i|module MatchPetri
    #{moduleComponentsSig}
    #{moduleInitialNodeRules}
    #{moduleNameRules}
    #{moduleReachabilityRules}
    #{modulePlantUMLSig}
    #{moduleExerciseRules}
    #{modules}

    #{singletonActions}
    #{singletonObjectNodes}

    pred showAd {
      #{predicates}
    }

    run showAd for #{scope} but #{bitWidth} Int, #{snd actionLimits} ActionNodes,
      #{snd objectNodeLimits} ObjectNodes, #{maxNamedNodes} ActionObjectNodes,
      #{snd actionLimits + snd objectNodeLimits} ComponentNames,
      exactly #{decisionMergePairs} DecisionNodes, exactly #{decisionMergePairs} MergeNodes,
      #{2 * decisionMergePairs} GuardNames, exactly #{forkJoinPairs} ForkNodes, exactly #{forkJoinPairs} JoinNodes,
      exactly 1 InitialNodes, exactly #{activityFinalNodes} ActivityFinalNodes, exactly #{flowFinalNodes} FlowFinalNodes,
      exactly #{cycles} PlantUMLRepeatBlocks, exactly #{decisionMergePairs - cycles} PlantUmlIfElseBlocks,
      exactly #{forkJoinPairs} PlantUMLForkBlocks
  |]
  where
    singletonActions :: String
singletonActions = [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map
      (\Int
x -> [i| one sig A#{x} extends ActionNodes {}|])
      [Int
1 .. (Int, Int) -> Int
forall a b. (a, b) -> a
fst (Int, Int)
actionLimits]
    singletonObjectNodes :: String
singletonObjectNodes = [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map
      (\Int
x -> [i| one sig O#{x} extends ObjectNodes {}|])
      [Int
1 .. (Int, Int) -> Int
forall a b. (a, b) -> a
fst (Int, Int)
objectNodeLimits]

adConfigScope :: AdConfig -> Int
adConfigScope :: AdConfig -> Int
adConfigScope AdConfig {
    Int
maxNamedNodes :: AdConfig -> Int
maxNamedNodes :: Int
maxNamedNodes,
    Int
decisionMergePairs :: AdConfig -> Int
decisionMergePairs :: Int
decisionMergePairs,
    Int
forkJoinPairs :: AdConfig -> Int
forkJoinPairs :: Int
forkJoinPairs
  } = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
maxNamedNodes Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
3 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
decisionMergePairs Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
4 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
forkJoinPairs

{-
 As of now, the highest Int-Value used in the Alloy Specification is 3 (#bodies in ForkBlocks),
 therefore 3 Bit (Two's Complement) should be enough.
 If this number is made configurable or the specification is changed to use larger Int values,
 this should be adapted.
-}
adConfigBitWidth :: AdConfig -> Int
adConfigBitWidth :: AdConfig -> Int
adConfigBitWidth = Int -> AdConfig -> Int
forall a b. a -> b -> a
const Int
3