Renamed merc_preorder to merc_refinement and extended the implementation with counter examples

[mlaveaux]

See the title, this is mostly to run the tests.

[Copilot]

Pull request overview

This PR renames the merc_preorder crate to merc_refinement and extends the implementation with counter example generation for failed refinement checks. The renaming better reflects the crate's purpose of checking refinement relations between labelled transition systems.

Changes:

• Renamed merc_preorder crate to merc_refinement with updated dependencies across the codebase
• Added counter example generation infrastructure including a CounterExampleConstructor and CounterExampleTree trait
• Enhanced refinement checking with new parameters for counter examples and preprocessing control
• Integrated timing measurements for rewrite operations and refinement checks
• Added JSON key-value formatting for structured logging in the vpg tool
• Fixed dependabot.yml configuration to enable Cargo ecosystem monitoring
• Minor documentation improvements and spelling corrections

Reviewed changes

Copilot reviewed 19 out of 22 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
Cargo.toml	Updated workspace member from crates/preorder to crates/refinement and enabled kv features for logging crates
Cargo.lock	Updated dependency references from merc_preorder to merc_refinement
tools/lts/Cargo.toml	Updated dependency from merc_preorder to merc_refinement
tools/lts/src/main.rs	Added CLI arguments for counter examples and preprocessing control, implemented counter example display
crates/refinement/Cargo.toml	Renamed package from merc_preorder to merc_refinement
crates/refinement/README.md	Updated documentation to reflect package rename and improved formatting
crates/refinement/src/lib.rs	Added exports for new counter example constructor module
crates/refinement/src/preorder.rs	Moved and updated from old location with new API for counter examples and preprocessing
crates/refinement/src/failures_refinement.rs	Extended refinement algorithm to support counter example generation with exploration strategy support
crates/refinement/src/counterexample_constructor.rs	New file implementing counter example tree construction and trace reconstruction
crates/refinement/src/antichain.rs	New file implementing antichain data structure for efficient state space exploration
tools/vpg/src/main.rs	Added JSON formatting for structured logging of key-value pairs
tools/rewrite/src/main.rs	Added timing infrastructure initialization and printing
tools/rewrite/src/lib.rs	Integrated timing measurements for rewrite operations
crates/vpg/src/variability_zielonka.rs	Enhanced debug logging with structured key-value pairs
crates/ldd/README.md	Reformatted citation for consistency
crates/aterm/README.md	Reformatted citations for consistency
SECURITY.md	Fixed grammatical errors ("featured" -> "feature", "send" -> "sent")
README.md	Fixed spelling ("MERC" -> "merc", "discussion" -> "discussions")
.github/dependabot.yml	Fixed configuration by setting package-ecosystem to "cargo" and removing comments

Comments suppressed due to low confidence (5)

crates/refinement/src/failures_refinement.rs:222

• The counter example functionality introduced in this PR lacks test coverage. The test only checks the case where counter_example is false. Consider adding tests that verify counter example generation works correctly, including both successful refinement (where no counter example is generated) and failed refinement (where a counter example should be returned).
  crates/refinement/src/failures_refinement.rs:45
• There is a spelling error in the documentation. "Brreadth-first" should be "Breadth-first".
  crates/refinement/src/failures_refinement.rs:171
• The doc comment for the LtsCache struct is empty (just "///"). This should either have actual documentation or be removed.
  crates/refinement/README.md:6
• There is a grammatical error. The sentence reads "which the preorder relation" but should be "which is the preorder relation" (missing "is").
  crates/refinement/src/failures_refinement.rs:178
• The LtsCache struct and its implementation appear to be unused code that was likely left in accidentally. The struct is empty, and the method returns an empty iterator. This dead code should be removed.

[Copilot]

The article should be "an" before "edge" (which starts with a vowel sound), not "a".

Suggested change

	/// Adds a edge to the counterexample tree.
	/// Adds an edge to the counterexample tree.

[Copilot]

The error message "Visiting log key-values failed" should be used in a proper error context. Using expect() with a panic message suggests this might be an unrecoverable error, but it's unclear if this is the intended behavior. Consider using a more graceful error handling approach or clarifying the failure scenario in the message.

Suggested change

	source.visit(&mut json_printer).expect("Visiting log key-values failed");
	if let Err(e) = source.visit(&mut json_printer) {
	return Err(std::io::Error::new(
	std::io::ErrorKind::Other,
	format!("visiting log key-values failed: {e}"),
	));
	}

[Copilot]

The if-let block should be combined with the else clause in a more idiomatic way. Consider printing the counter-example trace and then "false" together without the nested structure, or use a single println! for clarity.

Suggested change

	} else {
	if let Some(trace) = counter_example {
	println!("Counter-example trace:");
	for label in trace {
	println!(" {}", label);
	}
	}
	println!("false");
	} else if let Some(trace) = counter_example {
	println!("Counter-example trace:");
	for label in trace {
	println!(" {}", label);
	}
	println!("false");
	} else {
	println!("false");

[Copilot]

There is a spelling error in the comment. "three" should be "tree".

Suggested change

	/// The backward three is stored in a deque.
	/// The backward tree is stored in a deque.

[Copilot]

The unused import CounterExampleConstructor should be removed. It's imported but never used in this file.

Suggested change

use crate::CounterExampleConstructor;