tightbeam-rs 0.9.0

//! Configuration types for FDR refinement checking
//!
//! This module contains the core configuration structures and result types
//! used by the FDR exploration engine.

use std::collections::HashSet;
#[cfg(feature = "testing-fault")]
use std::{borrow::Cow, collections::HashMap, sync::Arc};

use crate::testing::error::TestingError;
use crate::testing::specs::csp::{Event, Process, State};

#[cfg(feature = "testing-fault")]
use crate::testing::fault::{ProcessEvent, ProcessState};
#[cfg(feature = "testing-fmea")]
use crate::testing::fmea::{FmeaConfig, FmeaReport};
#[cfg(feature = "testing-fault")]
use crate::{constants::DEFAULT_FAULT_SEED, error::TightBeamError, testing::error::FdrConfigError, utils::BasisPoints};

/// CSP trace: sequence of observable events
pub type Trace = Vec<Event>;

/// Refusal set: events refused in stable state
pub type RefusalSet = HashSet<Event>;

/// Failure: (trace, refusal_set)
pub type Failure = (Trace, RefusalSet);

/// Acceptance set: events accepted after trace
pub type AcceptanceSet = HashSet<Event>;

/// Scheduler model type
/// Panics if used when `testing-fault` feature is not enabled
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum SchedulerModel {
	/// Cooperative scheduling (yield-based)
	Cooperative,
	/// Preemptive scheduling (time-sliced)
	Preemptive,
}

/// Fault injection strategy for runtime and FDR-based fault injection
///
/// - **Deterministic**: Counter-based injection for reproducibility (DO-178C/IEC 61508)
/// - **Random**: Seeded RNG for statistical coverage (same seed = same faults)
#[cfg(feature = "testing-fault")]
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum InjectionStrategy {
	/// Deterministic fault injection (counter-based)
	/// Injects faults based on call counters: predictable, reproducible
	Deterministic,
	/// Random fault injection (seeded RNG)
	/// Injects faults probabilistically but deterministically via seed
	Random,
}

/// Individual fault injection configuration
#[cfg(feature = "testing-fault")]
#[derive(Clone)]
pub struct FaultInjection {
	pub error_factory: Arc<dyn Fn() -> TightBeamError + Send + Sync>,
	/// Probability in basis points (0-10000, where 10000 = 100%)
	/// Compile-time validated via BasisPoints type
	pub probability_bps: BasisPoints,
}

#[cfg(feature = "testing-fault")]
impl FaultInjection {
	/// Check if fault should fire based on RNG value (0-9999)
	pub fn should_inject(&self, rng_value: u32) -> bool {
		(rng_value % 10000) < (self.probability_bps.get() as u32)
	}
}

#[cfg(feature = "testing-fault")]
impl core::fmt::Debug for FaultInjection {
	fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
		f.debug_struct("FaultInjection")
			.field("probability_bps", &self.probability_bps)
			.finish_non_exhaustive()
	}
}

/// Fault model configuration with HashMap for O(1) lookups
/// Key: (csp_state, event_label)
/// Panics if used when `testing-fault` feature is not enabled
#[cfg(feature = "testing-fault")]
#[derive(Clone)]
pub struct FaultModel {
	pub injection_points: HashMap<(Cow<'static, str>, Cow<'static, str>), FaultInjection>,
	pub injection_strategy: InjectionStrategy,
	/// Seed for deterministic fault injection
	/// - reproducibility for DO-178C/IEC 61508
	pub seed: u64,
}

#[cfg(feature = "testing-fault")]
impl core::fmt::Debug for FaultModel {
	fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
		f.debug_struct("FaultModel")
			.field("injection_points", &format!("{} points", self.injection_points.len()))
			.field("injection_strategy", &self.injection_strategy)
			.finish()
	}
}

#[cfg(feature = "testing-fault")]
impl Default for FaultModel {
	fn default() -> Self {
		Self {
			injection_points: HashMap::new(),
			injection_strategy: InjectionStrategy::Deterministic,
			seed: DEFAULT_FAULT_SEED,
		}
	}
}

#[cfg(feature = "testing-fault")]
impl From<InjectionStrategy> for FaultModel {
	fn from(injection_strategy: InjectionStrategy) -> Self {
		Self { injection_points: HashMap::new(), injection_strategy, seed: DEFAULT_FAULT_SEED }
	}
}

#[cfg(feature = "testing-fault")]
impl FaultModel {
	/// Type-safe fault injection using ProcessState and ProcessEvent traits
	///
	/// Injects a fault at the specified (process state, event) combination with
	/// the given probability in basis points (0-10000, where 10000 = 100%).
	///
	/// Uses ProcessState and ProcessEvent traits for compile-time validation when
	/// used with enums generated by tb_process_spec! macro.
	pub fn with_fault<S, E, F, Err>(mut self, state: S, event: E, error_fn: F, probability_bps: BasisPoints) -> Self
	where
		S: ProcessState,
		E: ProcessEvent,
		F: Fn() -> Err + Send + Sync + 'static,
		Err: Into<TightBeamError>,
	{
		let key = (state.full_key(), Cow::Borrowed(event.event_label()));
		self.injection_points.insert(
			key,
			FaultInjection { error_factory: Arc::new(move || error_fn().into()), probability_bps },
		);
		self
	}

	/// Set seed for deterministic fault injection
	pub fn with_seed(mut self, seed: u64) -> Self {
		self.seed = seed;
		self
	}
}

/// FDR configuration for refinement checking and multi-seed exploration
///
/// Supports two modes:
/// 1. Single-process exploration: Verify properties of one process
/// 2. Refinement checking: Verify Spec ⊑ Impl (traces/failures/divergences)
#[derive(Debug, Clone)]
pub struct FdrConfig {
	/// Number of exploration seeds (different scheduling)
	pub seeds: u32,

	/// Maximum trace depth before cutoff
	pub max_depth: usize,

	/// Maximum consecutive τ-transitions before divergence detection
	pub max_internal_run: usize,

	/// Per-seed timeout in milliseconds
	pub timeout_ms: u64,

	/// Additional processes for refinement checking
	/// If provided, check: specs\[0\] ⊑ main_process
	pub specs: Vec<Process>,

	/// Stop refinement checking on first violation (fast-fail mode)
	/// When true (default), returns immediately after finding first counter-example
	/// When false, checks all specs and collects all violations
	pub fail_fast: bool,

	/// Expect FDR refinement to fail (for negative tests)
	/// When true, the test passes if refinement fails (proving the trace violates the spec)
	/// When false (default), the test fails if refinement fails
	pub expect_failure: bool,

	/// Number of schedulers (m) - for resource constraint modeling
	/// When m < n (process_count), some traces become impossible
	/// Optional: set to Some(_) to enable scheduler modeling, None to disable.
	/// When set, both scheduler_count and process_count must be Some(_).
	#[cfg(feature = "testing-fault")]
	pub scheduler_count: Option<u32>,

	/// Number of concurrent processes (n) - for resource constraint modeling
	/// Optional: set to Some(_) to enable scheduler modeling, None to disable.
	/// When set, both scheduler_count and process_count must be Some(_).
	#[cfg(feature = "testing-fault")]
	pub process_count: Option<u32>,

	/// Scheduler model type (Cooperative or Preemptive)
	/// Panics if set to Some(_) when `testing-fault` feature is not enabled
	pub scheduler_model: Option<SchedulerModel>,

	/// Fault injection model
	/// When provided, enables CSP state-driven fault injection during FDR exploration
	#[cfg(feature = "testing-fault")]
	pub fault_model: Option<FaultModel>,

	/// FMEA configuration
	#[cfg(feature = "testing-fmea")]
	pub fmea_config: Option<FmeaConfig>,
}

impl Default for FdrConfig {
	fn default() -> Self {
		Self {
			seeds: 64,
			max_depth: 128,
			max_internal_run: 32,
			timeout_ms: 5000,
			specs: Vec::new(),
			fail_fast: true,
			expect_failure: false,
			scheduler_model: None,
			#[cfg(feature = "testing-fault")]
			scheduler_count: None,
			#[cfg(feature = "testing-fault")]
			process_count: None,
			#[cfg(feature = "testing-fault")]
			fault_model: None,
			#[cfg(feature = "testing-fmea")]
			fmea_config: None,
		}
	}
}

impl FdrConfig {
	/// Validate scheduler model constraints with detailed error messages.
	///
	/// Checks:
	/// - scheduler_count and process_count must both be Some(_) or both be None
	/// - If set, scheduler_count must be <= process_count
	/// - If set, scheduler_count and process_count must be > 0
	///
	/// Returns `Ok(())` if validation passes, or a `TestingError` if validation fails.
	#[cfg(feature = "testing-fault")]
	pub fn validate_scheduler_model(&self) -> Result<(), TestingError> {
		match (self.scheduler_count, self.process_count) {
			(None, None) => Ok(()), // Scheduler modeling disabled - valid
			(Some(_), None) | (None, Some(_)) => Err(TestingError::InvalidFdrConfig(FdrConfigError {
				field: "scheduler_count/process_count",
				reason: "both must be set or both be None for resource constraint modeling",
			})),
			(Some(scheduler_count), Some(process_count)) => {
				if scheduler_count > process_count {
					return Err(TestingError::InvalidFdrConfig(FdrConfigError {
						field: "scheduler_count",
						reason: "cannot exceed process_count (would make resource modeling meaningless)",
					}));
				}
				if scheduler_count == 0 {
					return Err(TestingError::InvalidFdrConfig(FdrConfigError {
						field: "scheduler_count",
						reason: "must be > 0",
					}));
				}
				if process_count == 0 {
					return Err(TestingError::InvalidFdrConfig(FdrConfigError {
						field: "process_count",
						reason: "must be > 0",
					}));
				}
				Ok(())
			}
		}
	}

	/// Validate all constraints (scheduler model).
	///
	/// This is a convenience method that calls `validate_scheduler_model()`.
	#[cfg(feature = "testing-fault")]
	pub fn validate(&self) -> Result<(), TestingError> {
		self.validate_scheduler_model()
	}

	/// Validate all constraints (no-op when testing-fault is not enabled).
	#[cfg(not(feature = "testing-fault"))]
	pub fn validate(&self) -> Result<(), TestingError> {
		Ok(())
	}
}

/// Record of an injected fault during FDR exploration
#[cfg(feature = "testing-fault")]
#[derive(Debug, Clone, PartialEq)]
pub struct InjectedFaultRecord {
	pub csp_state: String,
	pub event_label: String,
	pub error_message: String,
	pub probability_bps: u16,
}

/// FDR verification verdict
///
/// Captures verification results from multi-seed exploration and refinement checking:
/// - Single-process properties: determinism, deadlock, divergence
/// - Refinement checking: Spec ⊑ Impl (traces, failures, divergences)
#[derive(Debug, Clone, PartialEq)]
pub struct FdrVerdict {
	/// Overall pass/fail status
	pub passed: bool,

	/// Whether analysis ran without hitting resource bounds or timeouts
	///
	/// False when trace/failure sets were truncated (bounded claim) or a
	/// refinement check was inconclusive. See the type-level docs.
	pub complete: bool,

	/// Divergence freedom: no infinite τ-loops detected
	pub divergence_free: bool,

	/// Deadlock freedom: no unexpected STOP states
	pub deadlock_free: bool,

	/// Determinism: structural proof that the LTS is deterministic
	///
	/// True only when the process has no hidden (τ) actions and no
	/// multi-target `(state, event)` transition -- a sufficient structural
	/// condition for CSP determinism (Roscoe 2010, §10.5). Informational:
	/// nondeterminism is a modeling choice, not a failure, so this flag
	/// does not affect `passed`.
	pub is_deterministic: bool,

	/// Trace refinement: traces(Impl) ⊆ traces(Spec)
	/// Only meaningful when specs provided in FdrConfig
	pub trace_refines: bool,

	/// Failures refinement: failures(Impl) ⊆ failures(Spec)
	/// Only meaningful when specs provided in FdrConfig
	pub failures_refines: bool,

	/// Divergence refinement: divergences(Impl) ⊆ divergences(Spec)
	/// Only meaningful when specs provided in FdrConfig
	pub divergence_refines: bool,

	/// Witness to trace refinement violation: trace in Impl but not in Spec
	pub trace_refinement_witness: Option<Trace>,

	/// Witness to failures refinement violation: (trace, refusal) in Impl but not in Spec
	pub failures_refinement_witness: Option<Failure>,

	/// Witness to divergence refinement violation: divergent trace in Impl but not in Spec
	pub divergence_refinement_witness: Option<Trace>,

	/// Witness to structural nondeterminism: first `(state, event)` with a
	/// hidden action or multiple transition targets (sorted state order,
	/// reproducible)
	pub determinism_witness: Option<(State, Event)>,

	/// Witness to divergence: (seed, τ-loop sequence) if found
	pub divergence_witness: Option<(u64, Vec<Event>)>,

	/// Witness to deadlock: (seed, trace, state) if found
	pub deadlock_witness: Option<(u64, Trace, State)>,

	/// Traces explored across all seeds
	pub traces_explored: usize,

	/// Distinct states visited
	pub states_visited: usize,

	/// Number of seeds successfully completed
	pub seeds_completed: u32,

	/// Seed that caused failure, if any
	pub failing_seed: Option<u64>,

	/// Number of exploration branches pruned for timing violations
	///
	/// Timed exploration drops branches whose WCET/deadline constraints
	/// fail. A non-zero count means model-level timing violations exist
	/// even though the surviving paths passed.
	pub timing_pruned: usize,

	/// Faults that were injected during exploration
	#[cfg(feature = "testing-fault")]
	pub faults_injected: Vec<InjectedFaultRecord>,

	/// Seeds that completed (reached exhaustion or terminal states)
	/// despite at least one injected fault suppressing a transition
	#[cfg(feature = "testing-fault")]
	pub error_recovery_successful: usize,

	/// Seeds that deadlocked or diverged after at least one injected
	/// fault suppressed a transition
	#[cfg(feature = "testing-fault")]
	pub error_recovery_failed: usize,

	/// FMEA report
	#[cfg(feature = "testing-fmea")]
	pub fmea_report: Option<FmeaReport>,
}

impl Default for FdrVerdict {
	fn default() -> Self {
		Self {
			passed: true,
			complete: true,
			divergence_free: true,
			deadlock_free: true,
			is_deterministic: true,
			trace_refines: true,
			failures_refines: true,
			divergence_refines: true,
			trace_refinement_witness: None,
			failures_refinement_witness: None,
			divergence_refinement_witness: None,
			determinism_witness: None,
			divergence_witness: None,
			deadlock_witness: None,
			traces_explored: 0,
			states_visited: 0,
			seeds_completed: 0,
			failing_seed: None,
			timing_pruned: 0,
			#[cfg(feature = "testing-fault")]
			faults_injected: Vec::new(),
			#[cfg(feature = "testing-fault")]
			error_recovery_successful: 0,
			#[cfg(feature = "testing-fault")]
			error_recovery_failed: 0,
			#[cfg(feature = "testing-fmea")]
			fmea_report: None,
		}
	}
}

#[cfg(test)]
mod tests {
	use super::*;
	use crate::testing::specs::csp::TransitionRelation;

	// ========== FaultModel Unit Tests ==========

	#[cfg(feature = "testing-fault")]
	mod fault_model {
		use super::*;

		#[derive(Debug, Clone, Copy)]
		struct TestError;

		impl core::fmt::Display for TestError {
			fn fmt(&self, f: &mut core::fmt::Formatter) -> core::fmt::Result {
				write!(f, "test error")
			}
		}

		impl From<TestError> for TightBeamError {
			fn from(e: TestError) -> Self {
				TightBeamError::InjectedFault(Box::new(e))
			}
		}

		#[derive(Debug, Clone, Copy)]
		struct TestState;

		impl ProcessState for TestState {
			fn process_name(&self) -> &'static str {
				"TestProcess"
			}
			fn state_name(&self) -> &'static str {
				"TestState"
			}
		}

		#[derive(Debug, Clone, Copy)]
		struct TestEvent;

		impl ProcessEvent for TestEvent {
			fn event_label(&self) -> &'static str {
				"test_event"
			}
		}

		#[derive(Debug, Clone, Copy)]
		struct AnotherState;

		impl ProcessState for AnotherState {
			fn process_name(&self) -> &'static str {
				"TestProcess"
			}
			fn state_name(&self) -> &'static str {
				"AnotherState"
			}
		}

		#[derive(Debug, Clone, Copy)]
		struct AnotherEvent;

		impl ProcessEvent for AnotherEvent {
			fn event_label(&self) -> &'static str {
				"another_event"
			}
		}

		#[test]
		fn default_initializes_empty() {
			let model = FaultModel::default();
			assert_eq!(model.injection_points.len(), 0);
			assert_eq!(model.injection_strategy, InjectionStrategy::Deterministic);
		}

		#[test]
		fn from_strategy_sets_strategy() {
			let model = FaultModel::from(InjectionStrategy::Random);
			assert_eq!(model.injection_strategy, InjectionStrategy::Random);
		}

		#[test]
		fn with_fault_adds_typed_injection() {
			let model = FaultModel::default().with_fault(TestState, TestEvent, || TestError, BasisPoints::new(5000));
			assert_eq!(model.injection_points.len(), 1);

			let key = (Cow::Borrowed("TestProcess.TestState"), Cow::Borrowed("test_event"));
			let injection = model.injection_points.get(&key).unwrap();
			assert_eq!(injection.probability_bps, BasisPoints::new(5000));
		}

		#[test]
		fn with_fault_io_error() {
			let model = FaultModel::default().with_fault(
				TestState,
				TestEvent,
				|| std::io::Error::new(std::io::ErrorKind::ConnectionRefused, "test"),
				BasisPoints::new(100),
			);

			let key = (Cow::Borrowed("TestProcess.TestState"), Cow::Borrowed("test_event"));
			let error = (model.injection_points.get(&key).unwrap().error_factory)();
			assert!(matches!(error, TightBeamError::IoError(_)));
		}

		#[test]
		fn hashmap_provides_o1_lookup() {
			let model = FaultModel::default()
				.with_fault(TestState, TestEvent, || TestError, BasisPoints::new(1000))
				.with_fault(TestState, AnotherEvent, || TestError, BasisPoints::new(2000))
				.with_fault(AnotherState, TestEvent, || TestError, BasisPoints::new(3000));
			assert_eq!(model.injection_points.len(), 3);

			let key1 = (Cow::Borrowed("TestProcess.TestState"), Cow::Borrowed("test_event"));
			let key2 = (Cow::Borrowed("TestProcess.TestState"), Cow::Borrowed("another_event"));
			let key3 = (Cow::Borrowed("TestProcess.AnotherState"), Cow::Borrowed("test_event"));
			assert_eq!(
				model.injection_points.get(&key1).unwrap().probability_bps,
				BasisPoints::new(1000)
			);
			assert_eq!(
				model.injection_points.get(&key2).unwrap().probability_bps,
				BasisPoints::new(2000)
			);
			assert_eq!(
				model.injection_points.get(&key3).unwrap().probability_bps,
				BasisPoints::new(3000)
			);
		}

		#[test]
		fn should_inject_probability_0_percent() {
			let model = FaultModel::default().with_fault(TestState, TestEvent, || TestError, BasisPoints::new(0));
			let key = (Cow::Borrowed("TestProcess.TestState"), Cow::Borrowed("test_event"));
			let injection = model.injection_points.get(&key).unwrap();
			assert!(!injection.should_inject(0));
			assert!(!injection.should_inject(9999));
		}

		#[test]
		fn should_inject_probability_100_percent() {
			let model = FaultModel::default().with_fault(TestState, TestEvent, || TestError, BasisPoints::new(10000));
			let key = (Cow::Borrowed("TestProcess.TestState"), Cow::Borrowed("test_event"));
			let injection = model.injection_points.get(&key).unwrap();
			assert!(injection.should_inject(0));
			assert!(injection.should_inject(9999));
		}

		#[test]
		fn should_inject_probability_50_percent() {
			let model = FaultModel::default().with_fault(TestState, TestEvent, || TestError, BasisPoints::new(5000));
			let key = (Cow::Borrowed("TestProcess.TestState"), Cow::Borrowed("test_event"));
			let injection = model.injection_points.get(&key).unwrap();
			assert!(injection.should_inject(0));
			assert!(injection.should_inject(4999));
			assert!(!injection.should_inject(5000));
			assert!(!injection.should_inject(9999));
		}

		#[test]
		#[should_panic(expected = "BasisPoints must be 0-10000")]
		fn probability_above_10000_panics() {
			let _model = FaultModel::default().with_fault(TestState, TestEvent, || TestError, BasisPoints::new(10001));
		}

		#[test]
		fn clone_preserves_injection_points() {
			let model1 = FaultModel::default().with_fault(TestState, TestEvent, || TestError, BasisPoints::new(5000));
			let model2 = model1.clone();
			assert_eq!(model2.injection_points.len(), 1);
			assert_eq!(model2.injection_strategy, InjectionStrategy::Deterministic);
		}
	}

	// ========== FdrConfig Tests ==========

	#[test]
	fn default_configuration() {
		let config = FdrConfig::default();
		assert_eq!(config.seeds, 64);
		assert_eq!(config.max_depth, 128);
		assert_eq!(config.max_internal_run, 32);
		assert_eq!(config.timeout_ms, 5000);
		assert!(config.specs.is_empty());
		assert!(config.fail_fast);
	}

	#[test]
	fn dual_mode_support() {
		// Mode 1: Single-process exploration
		let config_exploration = FdrConfig::default();
		assert!(config_exploration.specs.is_empty());

		// Mode 2: Refinement checking
		let spec = Process {
			name: "Spec",
			description: Some("Test spec"),
			initial: State("S0"),
			states: vec![State("S0")].into_iter().collect(),
			observable: HashSet::new(),
			hidden: HashSet::new(),
			choice: HashSet::new(),
			terminal: vec![State("S0")].into_iter().collect(),
			transitions: TransitionRelation::new(),
			#[cfg(feature = "testing-timing")]
			timing_constraints: None,
			#[cfg(feature = "testing-timing")]
			timed_transitions: None,
			#[cfg(feature = "testing-schedulability")]
			schedulability_periods: None,
		};

		let config_refinement = FdrConfig { specs: vec![spec], ..FdrConfig::default() };
		assert!(!config_refinement.specs.is_empty());
	}

	// ========== FdrVerdict Tests ==========

	#[test]
	fn verdict_default_all_pass() {
		let verdict = FdrVerdict::default();
		assert!(verdict.passed);
		assert!(verdict.divergence_free);
		assert!(verdict.deadlock_free);
		assert!(verdict.is_deterministic);
		assert_eq!(verdict.traces_explored, 0);
		assert_eq!(verdict.states_visited, 0);
	}

	#[test]
	fn verdict_tracks_witnesses() {
		let mut verdict = FdrVerdict::default();

		let trace = vec![Event("unexpected")];
		verdict.trace_refinement_witness = Some(trace.clone());
		assert_eq!(verdict.trace_refinement_witness, Some(trace));
	}
}