tightbeam-rs 0.6.2

//! CSPM Export for FDR4 Integration
//!
//! Provides functionality to export CSP processes to CSPM (CSP Machine-readable) format
//! for analysis with FDR4 model checker.

use std::io::Write;

use crate::testing::specs::composition::ProcessExpr;
use crate::testing::specs::csp::Process;

/// CSPM (CSP Machine-readable) export
pub struct CspmExporter<'a> {
	process: &'a Process,
}

impl<'a> CspmExporter<'a> {
	pub fn new(process: &'a Process) -> Self {
		Self { process }
	}

	/// Export process to CSPM format for FDR4
	pub fn export<W: Write>(&self, writer: &mut W) -> std::io::Result<()> {
		writeln!(writer, "-- Generated by tightbeam testing framework")?;
		writeln!(writer, "-- Process: {}", self.process.name)?;

		if let Some(desc) = self.process.description {
			writeln!(writer, "-- Description: {desc}")?;
		}

		writeln!(writer)?;

		// Observable alphabet
		self.write_datatype(writer, "Observable", "-- Observable alphabet (Σ)", &self.process.observable)?;

		// Hidden alphabet
		if !self.process.hidden.is_empty() {
			self.write_datatype(writer, "Hidden", "-- Hidden alphabet (τ)", &self.process.hidden)?;
		}

		// States
		self.write_datatype(writer, "States", "-- States", &self.process.states)?;

		// Process definition (simplified LTS representation)
		writeln!(writer, "-- Process: {}", self.process.name)?;
		writeln!(writer, "channel obs : Observable")?;
		writeln!(writer, "channel hid : Hidden")?;
		writeln!(writer)?;

		// Generate process per state
		for state in &self.process.states {
			write!(writer, "{}Process = ", state.0)?;

			if self.process.is_terminal(*state) {
				writeln!(writer, "SKIP")?;
			} else {
				// Get enabled actions
				let enabled = self.process.enabled(*state);

				if enabled.is_empty() {
					writeln!(writer, "STOP")?;
				} else {
					let mut first = true;
					for action in enabled {
						if !first {
							write!(writer, " [] ")?;
						}
						first = false;

						let next_states = self.process.step(*state, &action.event);
						let next = next_states.first().unwrap(); // Take first for simplicity

						if action.is_observable() {
							write!(writer, "obs.{} -> {}Process", action.event.0, next.0)?;
						} else {
							write!(writer, "hid.{} -> {}Process", action.event.0, next.0)?;
						}
					}
					writeln!(writer)?;
				}
			}
			writeln!(writer)?;
		}

		// Main process
		writeln!(
			writer,
			"{} = {}Process \\ {{| hid |}}",
			self.process.name, self.process.initial.0
		)?;

		Ok(())
	}

	/// Helper to write a CSPM datatype definition
	fn write_datatype<W: Write, T: std::fmt::Display>(
		&self,
		writer: &mut W,
		type_name: &str,
		comment: &str,
		items: &std::collections::HashSet<T>,
	) -> std::io::Result<()> {
		writeln!(writer, "{comment}")?;
		writeln!(writer, "datatype {type_name} = ")?;
		let mut iter = items.iter();
		if let Some(first) = iter.next() {
			write!(writer, "  {first}")?;
			for item in iter {
				write!(writer, " | {item}")?;
			}
			writeln!(writer)?;
		}
		writeln!(writer)?;
		Ok(())
	}

	/// Export a process expression (composition) to CSPM
	pub fn export_composition<W: Write>(expr: &ProcessExpr, writer: &mut W) -> std::io::Result<()> {
		writeln!(writer, "-- Generated by tightbeam testing framework")?;
		writeln!(writer, "-- Composition: {}", expr.name())?;
		writeln!(writer)?;

		Self::write_process_expr(expr, writer)?;

		Ok(())
	}

	/// Write a process expression recursively
	fn write_process_expr<W: Write>(expr: &ProcessExpr, writer: &mut W) -> std::io::Result<()> {
		match expr {
			ProcessExpr::Atomic { name: _, process } => {
				// Export the atomic process
				let exporter = CspmExporter::new(process);
				exporter.export(writer)?;
			}

			ProcessExpr::Synchronized { left, right } => {
				writeln!(writer, "-- Synchronized parallel: P || Q")?;

				Self::write_process_expr(left, writer)?;
				Self::write_process_expr(right, writer)?;

				writeln!(
					writer,
					"System = {} [| union(Events_{}, Events_{}) |] {}",
					left.name(),
					left.name(),
					right.name(),
					right.name()
				)?;
			}

			ProcessExpr::Interleaved { left, right } => {
				writeln!(writer, "-- Interleaved parallel: P ||| Q")?;

				Self::write_process_expr(left, writer)?;
				Self::write_process_expr(right, writer)?;

				writeln!(writer, "System = {} ||| {}", left.name(), right.name())?;
			}

			ProcessExpr::InterfaceParallel { left, sync_alphabet, right } => {
				writeln!(writer, "-- Interface parallel: P [| A |] Q")?;

				Self::write_process_expr(left, writer)?;
				Self::write_process_expr(right, writer)?;

				write!(writer, "System = {} [| {{", left.name())?;
				for (i, event) in sync_alphabet.iter().enumerate() {
					if i > 0 {
						write!(writer, ", ")?;
					}

					write!(writer, "{}", event.0)?;
				}

				writeln!(writer, "}} |] {}", right.name())?;
			}

			ProcessExpr::AlphabetizedParallel { left, left_alphabet, right_alphabet, right } => {
				writeln!(writer, "-- Alphabetized parallel: P [| αP | αQ |] Q")?;

				Self::write_process_expr(left, writer)?;
				Self::write_process_expr(right, writer)?;

				// Sync alphabet is intersection
				write!(writer, "AlphaP = {{")?;

				for (i, event) in left_alphabet.iter().enumerate() {
					if i > 0 {
						write!(writer, ", ")?;
					}
					write!(writer, "{}", event.0)?;
				}

				writeln!(writer, "}}")?;
				write!(writer, "AlphaQ = {{")?;

				for (i, event) in right_alphabet.iter().enumerate() {
					if i > 0 {
						write!(writer, ", ")?;
					}
					write!(writer, "{}", event.0)?;
				}

				writeln!(writer, "}}")?;
				writeln!(writer, "System = {} [| inter(AlphaP, AlphaQ) |] {}", left.name(), right.name())?;
			}

			ProcessExpr::Sequential { first, second } => {
				writeln!(writer, "-- Sequential composition: P ; Q")?;

				Self::write_process_expr(first, writer)?;
				Self::write_process_expr(second, writer)?;

				writeln!(writer, "System = {} ; {}", first.name(), second.name())?;
			}

			ProcessExpr::Hiding { process, hidden_events } => {
				writeln!(writer, "-- Hiding: P \\ A")?;

				Self::write_process_expr(process, writer)?;

				write!(writer, "HiddenEvents = {{")?;

				for (i, event) in hidden_events.iter().enumerate() {
					if i > 0 {
						write!(writer, ", ")?;
					}

					write!(writer, "{}", event.0)?;
				}

				writeln!(writer, "}}")?;
				writeln!(writer, "System = {} \\ HiddenEvents", process.name())?;
			}

			ProcessExpr::Renaming { process, mapping } => {
				writeln!(writer, "-- Renaming: P [[ old <- new ]]")?;

				Self::write_process_expr(process, writer)?;

				writeln!(writer, "System = {} [[", process.name())?;

				for (i, (old, new)) in mapping.iter().enumerate() {
					if i > 0 {
						writeln!(writer, ",")?;
					}

					write!(writer, "  {} <- {}", old.0, new.0)?;
				}

				writeln!(writer, "\n]]")?;
			}

			ProcessExpr::ExternalChoice { left, right } => {
				writeln!(writer, "-- External choice: P [] Q")?;

				Self::write_process_expr(left, writer)?;
				Self::write_process_expr(right, writer)?;

				writeln!(writer, "System = {} [] {}", left.name(), right.name())?;
			}

			ProcessExpr::InternalChoice { left, right } => {
				writeln!(writer, "-- Internal choice: P |~| Q")?;

				Self::write_process_expr(left, writer)?;
				Self::write_process_expr(right, writer)?;

				writeln!(writer, "System = {} |~| {}", left.name(), right.name())?;
			}
		}

		Ok(())
	}
}