From cb8b25d0e01aad51e7657be74ef713fbd46bad9e Mon Sep 17 00:00:00 2001 From: pmbittner Date: Fri, 5 Jul 2024 14:19:44 +0200 Subject: [PATCH] README: fix more broken links --- README.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index bda46422..237a5d3a 100644 --- a/README.md +++ b/README.md @@ -240,7 +240,7 @@ In particular, our library provides, The library is organized as follows: - The [src/Framework](src/Framework) directory contains the definitions of our formal framework, defined in Section 4 in our paper. - - [VariabilityLanguage.lagda.md](src/Framework/VariabilityLanguage.agda) defines variability languages and their denotational semantics. + - [VariabilityLanguage.agda](src/Framework/VariabilityLanguage.agda) defines variability languages and their denotational semantics. - Soundness and completeness are defined in the [Properties](src/Framework/Properties) sub-directory. - Definitions for expressiveness and configuration equivalence are in the [Relation](src/Framework/Relation) sub-directory. - Theorems for proofs for free (Section 4.4) are within the [Proof](src/Framework/Proof) sub-directory, including several additional interesting theorems, which did not fit into the paper. @@ -341,7 +341,7 @@ The following table shows where each of the definitions, theorems, and proofs fr | | Gruler's Language | `Gruler` | [src/Lang/Gruler.agda](src/Lang/Gruler.agda) | | | | Option Calculus | `WFOC`, `OC` | [src/Lang/OC.lagda.md](src/Lang/OC.lagda.md) | In contrast to the paper, WFOC duplicates the artifact constructor to enforce the existence of a top-level artifact. | | | Feature Structure Trees | `FST` | [src/Lang/FST.agda](src/Lang/FST.lagda.md) | | -| | Clone-and-Own (List of Variants) | `VariantList` | [src/Lang/VariantList.agda](src/Lang/VariantList.agda) | | +| | Clone-and-Own (List of Variants) | `VariantList` | [src/Lang/VariantList.lagda.md](src/Lang/VariantList.lagda.md) | | | Definition 4.1 | Indexed Set | `IndexedSet` | [src/Data/IndexedSet.lagda.md](src/Data/IndexedSet.lagda.md) | | | Definition 4.3 | Indexed Set Inclusion ⋿ | `_∈_` | [src/Data/IndexedSet.lagda.md](src/Data/IndexedSet.lagda.md) | | | | Subset ⊑ | `_⊆_`, `_⊆[_]_` | [src/Data/IndexedSet.lagda.md](src/Data/IndexedSet.lagda.md) | In contrast to `_⊆_`, `_⊆[_]_` requires an explicit mapping between the indices of the two indexed sets which can be useful information. | @@ -354,8 +354,8 @@ The following table shows where each of the definitions, theorems, and proofs fr | Definition 4.10 | Semantic Domain | `VMap` | [src/Framework/VariantMap.agda](src/Framework/VariantMap.agda) | In contrast to a variant map, the semantic domain is the type of variant maps instead of its elements. | | Definition 4.11 | configuration language 𝐶 | `ℂ` | [src/Framework/Definitions.agda](src/Framework/Definitions.agda) | | | Definition 4.12 | variability language 𝐿 | `𝔼` | [src/Framework/Definitions.agda](src/Framework/Definitions.agda) | | -| Definition 4.13 | ⟦.⟧ | `𝔼-Semantics` | [src/Framework/VariabilityLanguage.lagda.md](src/Framework/VariabilityLanguage.lagda.md) | | -| | | `VariabilityLanguage` | [src/Framework/VariabilityLanguage.lagda.md](src/Framework/VariabilityLanguage.lagda.md) | VariabilityLanguage is a bundle of 𝔼, 𝕂 and 𝔼-Semantics. | +| Definition 4.13 | ⟦.⟧ | `𝔼-Semantics` | [src/Framework/VariabilityLanguage.agda](src/Framework/VariabilityLanguage.agda) | | +| | | `VariabilityLanguage` | [src/Framework/VariabilityLanguage.agda](src/Framework/VariabilityLanguage.agda) | VariabilityLanguage is a bundle of 𝔼, 𝕂 and 𝔼-Semantics. | | Definition 4.15 | Complete(𝐿) | `Complete` | [src/Framework/Properties/Completeness.lagda.md](src/Framework/Properties/Completeness.lagda.md) | | | Definition 4.16 | Sound(𝐿) | `Sound` | [src/Framework/Properties/Soundness.lagda.md](src/Framework/Properties/Soundness.lagda.md) | | | Definition 4.17 | ⪰ | `_≽_` | [src/Framework/Relation/Expressiveness.lagda.md](src/Framework/Relation/Expressiveness.lagda.md) | | @@ -389,7 +389,7 @@ The following table shows where each of the definitions, theorems, and proofs fr | Corollary 5.13 | Sound(OC) | `OC-is-sound` | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md) | | | Theorem 5.14 | ¬Complete(OC) | `OC-is-incomplete` | [src/Lang/OC.lagda.md](src/Lang/OC.lagda.md) | | | Theorem 5.15 | 2CC ≻ OC | `2CC≻WFOC` | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md) | | -| Theorem 5.16 | ¬Complete(FST) | `FST-is-incomplete` | [src/Lang/FST.agda](src/Lang/FST.agda) | | +| Theorem 5.16 | ¬Complete(FST) | `FST-is-incomplete` | [src/Lang/FST.lagda.md](src/Lang/FST.lagda.md) | | | Theorem 5.17 | OC ⋡ FST | `WFOC⋡FST` | [src/Translation/Lang/FST-to-OC.lagda.md](src/Translation/Lang/FST-to-OC.lagda.md) | | | Theorem 5.18 | FST ⋡ OC | `FSTL⋡WFOCL` | [src/Translation/Lang/OC-to-FST.agda](src/Translation/Lang/OC-to-FST.agda) | | | Corollary 5.19 | FST ⋡ 2CC | `FST⋡2CC` | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md) | |