状態遷移表をAlloyに変換する(改訂版)

状態遷移表をAlloyスクリプトに変換するツールの改訂版。
StateTableモジュールを使用して状態遷移表を読み込む。

open StateTable
module main =
  let (states,variables,actions,values,transitions) =
    let dir = System.IO.Directory.GetCurrentDirectory()
    (dir + @"\sample.xlsx","Sheet1")
      |> ToStateTable
  
  type StateExp = string
  type StateExtendsExp = string
  type ActionExtendsExp = string
  type VariableExp = string
  type FactExp = string
  type Script = string 
  
  type ToStateExp = Variable[] -> StateExp
  type ToStateExttensExp = State[] -> StateExtendsExp
  type ToVariableExp = Variable[]*Value[] ->VariableExp
  type ToActionExtendsExp = Action[] -> ActionExtendsExp
  type ToFactExp = State[]*Variable[]*Action[] -> FactExp
  type ToScript = StateExp*VariableExp*ActionExtendsExp*FactExp -> Script
  
  let ToStateExp (variables:string[]):StateExp =
      [|"abstract sig State{";
        [|for i in 0..variables.Length-1 do yield (sprintf "  %s:t%s," variables.[i] variables.[i])|]
          |> String.concat "\n";           
        "  遷移:set Action->State\n}"
      |] |> String.concat "\n"
  
  let ToStateExtendsExp (states:string[]):StateExtendsExp =
    (states |> String.concat ",") |> sprintf "one sig %s extends State{}"
  
  let ToVariableExp ((variables:string[]),(values:string[][])):VariableExp =
    [|for i in 0..variables.Length-1 do
        let elms = [| for j in 0..values.Length-1 do yield values.[j].[i]|]
                      |> Set.ofArray
                      |> Set.map (fun elm->"v"+elm)
                      |> String.concat ","
        yield(sprintf"enum t%s{%s}" variables.[i] elms)|]
      |> String.concat "\n"
  
  let ToActionExtendsExp (actions:string[]):ActionExtendsExp =
    ([|for i in 0..actions.Length-1 do yield(sprintf"a%s" actions.[i])|] |> String.concat ",")
      |> sprintf "one sig %s extends Action{}"
  
  let ToFactExp ((states:State[]),(variables:Variable[]),(actions:Action[])):FactExp = 
    [|"fact{";
      [|for i in 0..states.Length-1 do
          for j in 0..variables.Length-1 do    
            yield (sprintf "  %s.%s=v%s" states.[i] variables.[j] values.[i].[j])|] 
        |> String.concat "\n";
      "遷移=";
      [|for i in 0..states.Length-1 do
          for j in 0..actions.Length-1 do
            let exp = sprintf "  %s->a%s->%s" states.[i] actions.[j] transitions.[i].[j]
            match transitions.[i].[j] with
            | "×" -> "" |> ignore
            |_-> yield exp          
      |] 
        |> String.concat " +\n";
      "}"|] |> String.concat "\n"
  
  let ToScript (stateExp,stateExtExp, variableExp, actionExp, factExp) :Script =
    [|stateExp;
      stateExtExp;
      variableExp;
      "abstract sig Action{}";
      actionExp;
      factExp;
      "run{}"|] |> String.concat "\n"
  
  let stateExp:StateExp = variables |> ToStateExp
  let stateExtExp:StateExtendsExp = states |> ToStateExtendsExp
  let variableExp:VariableExp = (variables,values) |> ToVariableExp
  let actionExp:ActionExtendsExp = actions |> ToActionExtendsExp
  let factExp:FactExp = (states,variables,actions) |> ToFactExp
  let script:Script = 
    (stateExp,stateExtExp,variableExp,actionExp,factExp) |> ToScript
    
  System.IO.File.WriteAllText("alloy.txt",script)