状態遷移表をAlloyスクリプトに変換する

Excel上に記述した状態遷移表をF#プログラムでAlloyスクリプトに変換する。

状態遷移表

f:id:borsalino:20161010161329p:plain

Alloyスクリプト

abstract sig State{
  スイッチ:tスイッチ,
  レベル:tレベル,
  ファン:tファン,
  遷移:set Action->State
}
one sig S0,S1,S2,S3 extends State{}
enum tスイッチ{vオフ,vオン}
enum tレベル{v弱,v強}
enum tファン{v停止,v弱回転,v強回転}
abstract sig Action{}
one sig aオフ,aオン,a弱,a強 extends Action{}
fact{
  S0.スイッチ=vオフ
  S0.レベル=v弱
  S0.ファン=v停止
  S1.スイッチ=vオフ
  S1.レベル=v強
  S1.ファン=v停止
  S2.スイッチ=vオン
  S2.レベル=v弱
  S2.ファン=v弱回転
  S3.スイッチ=vオン
  S3.レベル=v強
  S3.ファン=v強回転
遷移=
  S0->aオン->S2 +
  S0->a強->S1 +
  S1->aオン->S3 +
  S1->a弱->S0 +
  S2->aオフ->S0 +
  S2->a強->S3 +
  S3->aオフ->S1 +
  S3->a弱->S2
}
run{}

変換ツール

open Microsoft.Office.Interop.Excel
open System.Runtime.InteropServices

type CellValue = string
type State = CellValue
type Variable = CellValue
type Value = CellValue
type Action = CellValue
type Trans = CellValue

type CellToValue = System.Object -> CellValue
type ColumnsToValues = Range -> CellValue[]
type RowsToValues = Range -> CellValue[]
type MatrixToValues = Range -> CellValue[][]


let CreateRange (cell:Range, rows:int, columns:int) =
  cell.Address() + ":" + cell.Offset(rows-1,columns-1).Address()
let CellToValue (cell:System.Object):CellValue = (cell:?>Range).Value2:?>CellValue
let ColumnsToValues (range:Range) =
  [|for i in 1..range.Columns.Count do yield (range.[1,i] |> CellToValue)|]
let RowsToValues (range:Range):CellValue[] =
  [|for i in 1..range.Rows.Count do yield (range.[i,1] |> CellToValue)|]
let MatrixToValues (range:Range):CellValue[][] =
  [|for i in 1..range.Rows.Count do 
      yield [|for j in 1..range.Columns.Count do 
                yield (range.[i,j] |> CellToValue)|]|]

let excel = ApplicationClass(Visible = false)
let dir = System.IO.Directory.GetCurrentDirectory() 
let workbooks = excel.Workbooks.Open(dir + @"\sample.xlsx")
let worksheet = workbooks.Sheets.["Sheet1"] :?> Worksheet

let StateRange = worksheet.Range("A2:A5") // .Range("State")
let VariableRange = worksheet.Range("B1:D1") // .Range("Variable")
let ActionRange = worksheet.Range("E1:H1") // .Range("Action")
let ValueRange =
  (VariableRange.[2,1]:?>Range,
   StateRange.Rows.Count,
   VariableRange.Columns.Count) |> CreateRange
let TransitionsRange =
  (ActionRange.[2,1]:?>Range,
   StateRange.Rows.Count,
   ActionRange.Columns.Count) |> CreateRange
    
let states = StateRange |> RowsToValues
let variables = VariableRange |> ColumnsToValues
let actions = ActionRange |> ColumnsToValues
let values = worksheet.Range(ValueRange) |> MatrixToValues
let transitions = worksheet.Range(TransitionsRange) |> MatrixToValues

type StateExp = string
type StateExtExp = string
type ActionExp = string
type VariableExp = string
type FactExp = string
type Script = string 

type ToStateExp = Variable[] -> StateExp
type ToStateExtExp = State[] -> StateExtExp
type ToVariableExp = Variable[]*Value[] ->VariableExp
type ToActionExp = Action[] -> ActionExp
type ToFactExp = State[]*Variable[]*Action[] -> FactExp
type ToScript = StateExp*VariableExp*ActionExp*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 ToStateExtExp (states:string[]):StateExtExp =
  (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 ToActionExp (actions:string[]):ActionExp =
  ([|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:StateExtExp = states |> ToStateExtExp
let variableExp:VariableExp = (variables,values) |> ToVariableExp
let actionExp:ActionExp = actions |> ToActionExp
let factExp:FactExp = (states,variables,actions) |> ToFactExp
let script:Script = 
  (stateExp,stateExtExp,variableExp,actionExp,factExp) |> ToScript

excel.Quit()
excel |> Marshal.ReleaseComObject |> ignore
  
System.IO.File.WriteAllText("alloy.txt",script)