using System;
using System.IO;
using FsCheck;
using FsCheck.Fluent;
using FsCheck.Xunit;
using XplorePlane.Helpers;
namespace XplorePlane.Tests.Helpers
{
///
/// FsCheck property-based tests for ManualImageValidator.
/// Property 4: ManualImagePath 验证正确性
/// **Validates: Requirements 2.1, 2.3**
///
public class ManualImageValidatorPropertyTests
{
// ── Generators ──────────────────────────────────────────────────────
///
/// Generates null, empty, or whitespace-only strings.
///
private static Gen NullOrWhitespaceGen()
{
return Gen.OneOf(
Gen.Constant((string)null),
Gen.Constant(string.Empty),
Gen.Constant(" "),
Gen.Constant(" "),
Gen.Constant("\t"),
Gen.Constant("\t \n"),
Gen.Constant(" \r\n "));
}
///
/// Generates paths longer than 260 characters (non-whitespace).
///
private static Gen PathTooLongGen()
{
// Generate lengths from 261 to 500
return Gen.Choose(261, 500).Select(len =>
{
// Use a valid-looking path prefix to ensure it's not whitespace
var prefix = @"C:\Images\";
var remaining = len - prefix.Length;
if (remaining <= 0) remaining = 1;
return prefix + new string('a', remaining);
});
}
///
/// Generates non-empty paths with length ≤ 260 that point to non-existent files.
/// Uses random alphanumeric characters to ensure the file won't exist.
///
private static Gen NonExistentPathGen()
{
// Generate a path that is very unlikely to exist on disk
var charGen = Gen.Elements(
'a', 'b', 'c', 'd', 'e', 'f', 'g', 'h', 'i', 'j',
'A', 'B', 'C', 'D', 'E', 'F', '0', '1', '2', '3');
return from len in Gen.Choose(5, 50)
from chars in Gen.ArrayOf(charGen).Resize(len)
select @"C:\NonExistent_" + new string(chars) + ".bmp";
}
// ── Property Tests ──────────────────────────────────────────────────
///
/// Property 4.1: Null/whitespace/empty paths always return Empty.
/// For any null, empty, or whitespace-only string, Validate SHALL return Empty.
///
[Property(MaxTest = 100)]
public Property NullOrWhitespacePaths_ReturnEmpty()
{
return Prop.ForAll(
NullOrWhitespaceGen().ToArbitrary(),
path =>
{
var result = ManualImageValidator.Validate(path);
return result == ManualImageValidationResult.Empty;
});
}
///
/// Property 4.2: Paths longer than 260 characters always return PathTooLong.
/// For any non-whitespace path with length > 260, Validate SHALL return PathTooLong.
///
[Property(MaxTest = 100)]
public Property PathsLongerThan260_ReturnPathTooLong()
{
return Prop.ForAll(
PathTooLongGen().ToArbitrary(),
path =>
{
var result = ManualImageValidator.Validate(path);
return result == ManualImageValidationResult.PathTooLong;
});
}
///
/// Property 4.3: Non-existent file paths (non-empty, ≤260) return FileNotFound.
/// For any non-whitespace path with length ≤ 260 that does not exist on disk,
/// Validate SHALL return FileNotFound.
///
[Property(MaxTest = 100)]
public Property NonExistentPaths_ReturnFileNotFound()
{
return Prop.ForAll(
NonExistentPathGen().ToArbitrary(),
path =>
{
var result = ManualImageValidator.Validate(path);
return result == ManualImageValidationResult.FileNotFound;
});
}
///
/// Property 4.4: The result is always one of the defined enum values (exhaustive classification).
/// For any arbitrary string, Validate SHALL return a value within the defined enum range.
///
[Property(MaxTest = 100)]
public Property Result_IsAlwaysDefinedEnumValue()
{
// Generate arbitrary strings including nulls, empty, whitespace, and random paths
var charGen = Gen.Frequency(
(5, Gen.Choose(0x20, 0x7E).Select(i => (char)i)), // printable ASCII
(2, Gen.Choose(0x4E00, 0x9FFF).Select(i => (char)i)), // CJK characters
(1, Gen.Elements('\\', '/', ':', '*', '?', '"', '<', '>', '|')),
(1, Gen.Elements(' ', '\t', '\n', '\r'))
);
var randomStringGen = from len in Gen.Choose(0, 300)
from chars in Gen.ArrayOf(charGen).Resize(len)
select new string(chars);
var anyStringGen = Gen.OneOf(
Gen.Constant((string)null),
Gen.Constant(string.Empty),
Gen.Constant(" "),
randomStringGen);
return Prop.ForAll(
anyStringGen.ToArbitrary(),
path =>
{
var result = ManualImageValidator.Validate(path);
return Enum.IsDefined(typeof(ManualImageValidationResult), result);
});
}
///
/// Property 4.5: Existing files with supported extensions return Valid.
/// Creates temporary files with supported extensions and verifies Validate returns Valid.
///
[Property(MaxTest = 20)]
public Property ExistingFilesWithSupportedExtension_ReturnValid()
{
var supportedExtGen = Gen.Elements(".bmp", ".png", ".tiff", ".tif");
return Prop.ForAll(
supportedExtGen.ToArbitrary(),
ext =>
{
var tempDir = Path.Combine(Path.GetTempPath(), "ManualImageValidatorTests");
Directory.CreateDirectory(tempDir);
var tempFile = Path.Combine(tempDir, $"test_{Guid.NewGuid():N}{ext}");
try
{
File.WriteAllBytes(tempFile, new byte[] { 0x00 });
var result = ManualImageValidator.Validate(tempFile);
return result == ManualImageValidationResult.Valid;
}
finally
{
if (File.Exists(tempFile))
File.Delete(tempFile);
}
});
}
///
/// Property 4.6: Existing files with unsupported extensions return UnsupportedFormat.
/// Creates temporary files with unsupported extensions and verifies Validate returns UnsupportedFormat.
///
[Property(MaxTest = 20)]
public Property ExistingFilesWithUnsupportedExtension_ReturnUnsupportedFormat()
{
var unsupportedExtGen = Gen.Elements(".jpg", ".jpeg", ".gif", ".svg", ".webp", ".txt", ".dat");
return Prop.ForAll(
unsupportedExtGen.ToArbitrary(),
ext =>
{
var tempDir = Path.Combine(Path.GetTempPath(), "ManualImageValidatorTests");
Directory.CreateDirectory(tempDir);
var tempFile = Path.Combine(tempDir, $"test_{Guid.NewGuid():N}{ext}");
try
{
File.WriteAllBytes(tempFile, new byte[] { 0x00 });
var result = ManualImageValidator.Validate(tempFile);
return result == ManualImageValidationResult.UnsupportedFormat;
}
finally
{
if (File.Exists(tempFile))
File.Delete(tempFile);
}
});
}
}
}