Skip to content

Commit

Permalink
Improve documentation
Browse files Browse the repository at this point in the history
- Update docs
- Avoid errors in CI due to concurrent runs of TLC
  • Loading branch information
vitorenesduarte committed Mar 31, 2021
1 parent f96b82e commit e3e859d
Show file tree
Hide file tree
Showing 23 changed files with 357 additions and 122 deletions.
15 changes: 15 additions & 0 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ jobs:
- uses: actions-rs/cargo@v1
with:
command: test
args: -- --test-threads=1

fmt:
name: Rustfmt
Expand All @@ -33,6 +34,20 @@ jobs:
command: fmt
args: --all -- --check

docs-build:
name: Documentation build
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v2
- uses: actions-rs/toolchain@v1
with:
profile: minimal
toolchain: stable
override: true
- uses: actions-rs/cargo@v1
with:
command: doc

clippy:
name: Clippy
runs-on: ubuntu-latest
Expand Down
15 changes: 0 additions & 15 deletions modelator/examples/json_trace.rs

This file was deleted.

1 change: 1 addition & 0 deletions modelator/src/artifact/json_trace.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
use serde_json::Value as JsonValue;

/// `modelator`'s artifact containing a test trace encoded as JSON.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct JsonTrace {
states: JsonValue,
Expand Down
10 changes: 10 additions & 0 deletions modelator/src/artifact/tla_cfg_file.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@ use crate::Error;
use std::convert::TryFrom;
use std::path::{Path, PathBuf};

/// `modelator`'s artifact representing a TLA+ config file containing the TLA+
/// model `CONSTANT`s and `INIT` and `NEXT` predicates.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct TlaConfigFile {
path: PathBuf,
Expand All @@ -14,6 +16,7 @@ impl TlaConfigFile {
Ok(Self { path })
}

/// Returns the path to the TLA+ config file.
pub fn path(&self) -> &PathBuf {
&self.path
}
Expand All @@ -22,6 +25,13 @@ impl TlaConfigFile {
// TODO: replace the following `TryFrom` implementations with one with generic
// bound `AsRef<Path>` once https://github.com/rust-lang/rust/issues/50133
// is fixed
impl TryFrom<&str> for TlaConfigFile {
type Error = crate::Error;
fn try_from(path: &str) -> Result<Self, Self::Error> {
Self::new(path)
}
}

impl TryFrom<String> for TlaConfigFile {
type Error = crate::Error;
fn try_from(path: String) -> Result<Self, Self::Error> {
Expand Down
9 changes: 9 additions & 0 deletions modelator/src/artifact/tla_file.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ use crate::Error;
use std::convert::TryFrom;
use std::path::{Path, PathBuf};

/// `modelator`'s artifact representing a TLA+ file.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct TlaFile {
path: PathBuf,
Expand All @@ -14,6 +15,7 @@ impl TlaFile {
Ok(Self { path })
}

/// Returns the path to the TLA+ file.
pub fn path(&self) -> &PathBuf {
&self.path
}
Expand All @@ -37,6 +39,13 @@ impl TlaFile {
// TODO: replace the following `TryFrom` implementations with one with generic
// bound `AsRef<Path>` once https://github.com/rust-lang/rust/issues/50133
// is fixed
impl TryFrom<&str> for TlaFile {
type Error = crate::Error;
fn try_from(path: &str) -> Result<Self, Self::Error> {
Self::new(path)
}
}

impl TryFrom<String> for TlaFile {
type Error = crate::Error;
fn try_from(path: String) -> Result<Self, Self::Error> {
Expand Down
1 change: 1 addition & 0 deletions modelator/src/artifact/tla_trace.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ use std::str::FromStr;

pub(crate) type TlaState = String;

/// `modelator`'s artifact containing a test trace encoded as TLA+.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct TlaTrace {
states: Vec<TlaState>,
Expand Down
17 changes: 8 additions & 9 deletions modelator/src/cli/mod.rs
Original file line number Diff line number Diff line change
@@ -1,15 +1,13 @@
// CLI output.
mod output;

// Re-exports.
pub use output::{CliOutput, CliStatus};
pub(crate) mod output;

use crate::artifact::{JsonTrace, TlaConfigFile, TlaFile, TlaTrace};
use crate::Error;
use clap::{AppSettings, Clap, Subcommand};
use serde_json::{json, Value as JsonValue};
use std::path::Path;

/// A struct that generates a CLI for `modelator` using [`clap`].
#[derive(Clap, Debug)]
#[clap(name = "modelator")]
#[clap(setting = AppSettings::DisableHelpSubcommand)]
Expand All @@ -30,7 +28,7 @@ enum Modules {

#[derive(Debug, Clap)]
#[clap(setting = AppSettings::DisableHelpSubcommand)]
pub enum TlaMethods {
enum TlaMethods {
/// Generate TLA+ tests.
GenerateTests {
/// TLA+ file with test cases.
Expand All @@ -47,7 +45,7 @@ pub enum TlaMethods {

#[derive(Debug, Clap)]
#[clap(setting = AppSettings::DisableHelpSubcommand)]
pub enum ApalacheMethods {
enum ApalacheMethods {
/// Generate TLA+ trace from a TLA+ test.
Test {
/// TLA+ file generated by the generate-test method in the TLA module.
Expand All @@ -64,7 +62,7 @@ pub enum ApalacheMethods {

#[derive(Debug, Clap)]
#[clap(setting = AppSettings::DisableHelpSubcommand)]
pub enum TlcMethods {
enum TlcMethods {
/// Generate TLA+ trace from a TLA+ test.
Test {
/// TLA+ file generated by the generate-test method in the TLA module.
Expand All @@ -75,9 +73,10 @@ pub enum TlcMethods {
}

impl CliOptions {
pub fn run(self) -> CliOutput {
/// Function that runs `modelator` given the parameters in the [CliOptions].
pub fn run(self) -> output::CliOutput {
let result = self.subcommand.run();
CliOutput::with_result(result)
output::CliOutput::with_result(result)
}
}

Expand Down
8 changes: 7 additions & 1 deletion modelator/src/cli/output.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,8 @@ use crate::Error;
use serde::Serialize;
use serde_json::Value as JsonValue;

/// Struct representing the output of `modelator` CLI.
/// See [super::CliOptions].
#[derive(Serialize, Debug)]
pub struct CliOutput {
/// The return status
Expand All @@ -30,6 +32,8 @@ impl CliOutput {
Self { status, result }
}

/// Function that exits the program with a proper error code given the
/// the [CliOutput].
pub fn exit(self) {
let pretty = match serde_json::to_string_pretty(&self) {
Ok(pretty) => pretty,
Expand All @@ -47,11 +51,13 @@ impl CliOutput {
}

/// Represents the exit status of any CLI command
#[derive(Serialize, Debug, PartialEq, Eq)]
#[derive(Serialize, Debug, PartialEq, Eq, Clone, Copy)]
pub enum CliStatus {
/// An exit status representing success.
#[serde(rename(serialize = "success"))]
Success,

/// An exit status representing an error.
#[serde(rename(serialize = "error"))]
Error,
}
46 changes: 23 additions & 23 deletions modelator/src/datachef.rs
Original file line number Diff line number Diff line change
Expand Up @@ -304,23 +304,23 @@ impl Recipe {
mod tests {
use super::*;

pub struct Record {
pub name: String,
pub address: Address,
pub landline: Phone,
pub mobile: Phone,
struct Record {
name: String,
address: Address,
landline: Phone,
mobile: Phone,
}

pub struct Address {
pub postal_code: u32,
pub city: String,
pub street: String,
pub door: u32,
struct Address {
postal_code: u32,
_city: String,
_street: String,
_door: u32,
}

pub struct Phone {
pub area_code: u32,
pub number: u32,
struct Phone {
area_code: u32,
_number: u32,
}

fn check_record(r: Record) -> bool {
Expand All @@ -343,13 +343,13 @@ mod tests {
let mut r = Recipe::new();
r.put(|_| Phone {
area_code: 123,
number: 456789,
_number: 456789,
});
r.put(|_| Address {
postal_code: 10179,
city: "Berlin".to_string(),
street: "Molkenmarkt".to_string(),
door: 1,
_city: "Berlin".to_string(),
_street: "Molkenmarkt".to_string(),
_door: 1,
});
r.add(|r, name: String| Record {
name,
Expand All @@ -364,7 +364,7 @@ mod tests {

r.add(|_, phone: (u32, u32)| Phone {
area_code: phone.0,
number: phone.1,
_number: phone.1,
});
r.add(|r, phone: (u32, u32)| Record {
name: "John Smith".to_string(),
Expand All @@ -389,35 +389,35 @@ mod tests {
}

#[derive(Debug, PartialEq)]
pub struct Chain {
struct Chain {
name: String,
id: u64,
default_provider: Provider,
}

#[derive(Debug, PartialEq)]
pub struct Provider {
struct Provider {
name: String,
id: u64,
}

#[derive(Debug, PartialEq)]
pub struct Block {
struct Block {
chain: Chain,
height: u64,
id: u64,
provider: Provider,
}

#[derive(Debug, PartialEq)]
pub struct AbstractBlock {
struct AbstractBlock {
chain: String,
height: u64,
provider: String,
}

#[test]
pub fn test() {
fn test() {
let mut r = Recipe::new();
r.put_as("height", |_| 1u64);
r.put_as("id", |_| 0u64);
Expand Down
Loading

0 comments on commit e3e859d

Please sign in to comment.