diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml new file mode 100644 index 0000000..3e98c5d --- /dev/null +++ b/.github/workflows/main.yml @@ -0,0 +1,27 @@ +name: Ruby + +on: + push: + branches: + - master + + pull_request: + +jobs: + build: + runs-on: ubuntu-latest + name: Ruby ${{ matrix.ruby }} + strategy: + matrix: + ruby: + - '2.6.6' + + steps: + - uses: actions/checkout@v3 + - name: Set up Ruby + uses: ruby/setup-ruby@v1 + with: + ruby-version: ${{ matrix.ruby }} + bundler-cache: true + - name: Run the default task + run: bundle exec rake diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..c6e6e4a --- /dev/null +++ b/.gitignore @@ -0,0 +1,13 @@ +/.bundle/ +/.yardoc +/_yardoc/ +/coverage/ +/pkg/ +/spec/reports/ +/tmp/ +/.vscode/ +NuSMV-*/ +program-graph.rb + +# rspec failure tracking +.rspec_status diff --git a/.rspec b/.rspec new file mode 100644 index 0000000..34c5164 --- /dev/null +++ b/.rspec @@ -0,0 +1,3 @@ +--format documentation +--color +--require spec_helper diff --git a/Gemfile b/Gemfile new file mode 100644 index 0000000..857a0bf --- /dev/null +++ b/Gemfile @@ -0,0 +1,10 @@ +# frozen_string_literal: true + +source "https://rubygems.org" + +# Specify your gem's dependencies in progg.gemspec +gemspec + +gem "rake", "~> 13.0" + +gem "rspec", "~> 3.0" diff --git a/Gemfile.lock b/Gemfile.lock new file mode 100644 index 0000000..3dcb593 --- /dev/null +++ b/Gemfile.lock @@ -0,0 +1,97 @@ +PATH + remote: . + specs: + progg (0.1.0) + config (~> 4.2.1) + ebnf (~> 2.3.4) + plantuml_builder (~> 0.3.0) + rainbow (~> 3.0.0) + thor (~> 1.2.1) + +GEM + remote: https://rubygems.org/ + specs: + concurrent-ruby (1.2.2) + config (4.2.1) + deep_merge (~> 1.2, >= 1.2.1) + dry-validation (~> 1.0, >= 1.0.0) + deep_merge (1.2.2) + diff-lcs (1.5.0) + docopt (0.5.0) + dry-configurable (0.13.0) + concurrent-ruby (~> 1.0) + dry-core (~> 0.6) + dry-container (0.9.0) + concurrent-ruby (~> 1.0) + dry-configurable (~> 0.13, >= 0.13.0) + dry-core (0.7.1) + concurrent-ruby (~> 1.0) + dry-inflector (0.2.1) + dry-initializer (3.0.4) + dry-logic (1.2.0) + concurrent-ruby (~> 1.0) + dry-core (~> 0.5, >= 0.5) + dry-schema (1.8.0) + concurrent-ruby (~> 1.0) + dry-configurable (~> 0.13, >= 0.13.0) + dry-core (~> 0.5, >= 0.5) + dry-initializer (~> 3.0) + dry-logic (~> 1.0) + dry-types (~> 1.5) + dry-types (1.5.1) + concurrent-ruby (~> 1.0) + dry-container (~> 0.3) + dry-core (~> 0.5, >= 0.5) + dry-inflector (~> 0.1, >= 0.1.2) + dry-logic (~> 1.0, >= 1.0.2) + dry-validation (1.7.0) + concurrent-ruby (~> 1.0) + dry-container (~> 0.7, >= 0.7.1) + dry-core (~> 0.5, >= 0.5) + dry-initializer (~> 3.0) + dry-schema (~> 1.8, >= 1.8.0) + ebnf (2.3.4) + htmlentities (~> 4.3) + rdf (~> 3.2) + scanf (~> 1.0) + sxp (~> 1.2) + unicode-types (~> 1.8) + htmlentities (4.3.4) + link_header (0.0.8) + matrix (0.4.2) + plantuml_builder (0.3.0) + docopt (~> 0.5.0) + rainbow (3.0.0) + rake (13.0.6) + rdf (3.2.11) + link_header (~> 0.0, >= 0.0.8) + rspec (3.12.0) + rspec-core (~> 3.12.0) + rspec-expectations (~> 3.12.0) + rspec-mocks (~> 3.12.0) + rspec-core (3.12.0) + rspec-support (~> 3.12.0) + rspec-expectations (3.12.1) + diff-lcs (>= 1.2.0, < 2.0) + rspec-support (~> 3.12.0) + rspec-mocks (3.12.1) + diff-lcs (>= 1.2.0, < 2.0) + rspec-support (~> 3.12.0) + rspec-support (3.12.0) + scanf (1.0.0) + sxp (1.2.4) + matrix (~> 0.4) + rdf (~> 3.2) + thor (1.2.1) + unicode-types (1.8.0) + +PLATFORMS + x86_64-darwin-19 + +DEPENDENCIES + progg! + rake (~> 13.0) + rspec (~> 3.0) + +BUNDLED WITH + 2.3.26 diff --git a/README.md b/README.md new file mode 100644 index 0000000..038e628 --- /dev/null +++ b/README.md @@ -0,0 +1,29 @@ +# Progg + +Welcome to your new gem! In this directory, you'll find the files you need to be able to package up your Ruby library into a gem. Put your Ruby code in the file `lib/progg`. To experiment with that code, run `bin/console` for an interactive prompt. + +TODO: Delete this and the text above, and describe your gem + +## Installation + +Install the gem and add to the application's Gemfile by executing: + + $ bundle add progg + +If bundler is not being used to manage dependencies, install the gem by executing: + + $ gem install progg + +## Usage + +TODO: Write usage instructions here + +## Development + +After checking out the repo, run `bin/setup` to install dependencies. Then, run `rake spec` to run the tests. You can also run `bin/console` for an interactive prompt that will allow you to experiment. + +To install this gem onto your local machine, run `bundle exec rake install`. To release a new version, update the version number in `version.rb`, and then run `bundle exec rake release`, which will create a git tag for the version, push git commits and the created tag, and push the `.gem` file to [rubygems.org](https://rubygems.org). + +## Contributing + +Bug reports and pull requests are welcome on GitHub at https://github.com/[USERNAME]/progg. diff --git a/Rakefile b/Rakefile new file mode 100644 index 0000000..b6ae734 --- /dev/null +++ b/Rakefile @@ -0,0 +1,8 @@ +# frozen_string_literal: true + +require "bundler/gem_tasks" +require "rspec/core/rake_task" + +RSpec::Core::RakeTask.new(:spec) + +task default: :spec diff --git a/bin/console b/bin/console new file mode 100755 index 0000000..a434a89 --- /dev/null +++ b/bin/console @@ -0,0 +1,15 @@ +#!/usr/bin/env ruby +# frozen_string_literal: true + +require "bundler/setup" +require "progg" + +# You can add fixtures and/or initialization code here to make experimenting +# with your gem easier. You can also use a different console, if you like. + +# (If you use this, don't forget to add pry to your Gemfile!) +# require "pry" +# Pry.start + +require "irb" +IRB.start(__FILE__) diff --git a/bin/progg.rb b/bin/progg.rb new file mode 100644 index 0000000..4534820 --- /dev/null +++ b/bin/progg.rb @@ -0,0 +1,31 @@ +require "bundler/setup" +require 'progg' + +module Progg + + class ProggCLI + + def run() + + Cli::BaseCommand.start() + # executor = Cli::CommandExecutor.new + + # executor.exec(ARGV) + + # self.parse(ARGV) + + # script = ProggScript.new() + # script.interpret('program-graph.rb') + + # if params[:help] + # print help + # elsif params.errors.any? + # puts params.errors.summary + # else + # pp params.to_h + # end + end + + end + +end diff --git a/bin/setup b/bin/setup new file mode 100755 index 0000000..dce67d8 --- /dev/null +++ b/bin/setup @@ -0,0 +1,8 @@ +#!/usr/bin/env bash +set -euo pipefail +IFS=$'\n\t' +set -vx + +bundle install + +# Do any other automated setup that you need to do here diff --git a/calc.ebnf b/calc.ebnf new file mode 100644 index 0000000..bd2392b --- /dev/null +++ b/calc.ebnf @@ -0,0 +1,21 @@ +[1] Assignment ::= VARIABLE ':=' IntExpr +[2] Expression ::= BoolExpr + +[3] BoolExpr ::= Equivalence +[4] Equivalence ::= Implication (('<->' | '') Implication)* +[5] Implication ::= Disjunction ('=>' Disjunction)* +[6] Disjunction ::= Konjunction ('||' Konjunction)* +[7] Konjunction ::= Negation ('&&' Negation)* +[8] Negation ::= '!' Comparison | Comparison + +[9] Comparison ::= Sum (CMPOP Sum)* + +[10] IntExpr ::= Sum +[11] Sum ::= Product (('+' | '-') Product)* +[12] Product ::= Value (('*' | '/') Value)* +[13] Value ::= NUMBER | BOOL | VARIABLE | '(' Expression ')' + +[14] NUMBER ::= [0-9]+ +[15] BOOL ::= 'true' | 'false' +[16] VARIABLE ::= [a-zA-Z_][a-zA-Z0-9_]* +[17] CMPOP ::= '<=' | '>=' | '<' | '>' | '==' | '!=' diff --git a/data/config/progg.yml b/data/config/progg.yml new file mode 100644 index 0000000..4c12203 --- /dev/null +++ b/data/config/progg.yml @@ -0,0 +1,25 @@ + +# The working directory for temporary files and caches +workdir: <%= File.expand_path('.progg', Dir.home) %> + +numsv: + path: /Users/arian/Documents/projects/progg/NuSMV-2.6.0-Darwin/bin/NuSMV + +# Enable/Disable colored printing all together +use_colors: true +# Enable/Disable colored printing when the output of vsutil +# is not piped into a TTY directly. +use_colors_in_pipe: false +# Colors theme for the TTY +colors: + state: ["deepskyblue", "bold"] + trans: [ "springgreen", "italic" ] + var: [ "limegreen", "italic" ] + cmp: ["deepskyblue", "bold", "italic"] + + num: dodgerblue + success: springgreen + warn: khaki + error: red + + sidenote: "darkslategray" diff --git a/data/config/theme.yml b/data/config/theme.yml new file mode 100644 index 0000000..15458fd --- /dev/null +++ b/data/config/theme.yml @@ -0,0 +1,13 @@ + + + +prompt: + prompt_format: " %s" + debug: "D " + verbose: "V " + info: "➜ " + warn: "⚡" + error: "✘ " + empty: "~ " + success: "✓ " + question: "» " \ No newline at end of file diff --git a/devprogg b/devprogg new file mode 100755 index 0000000..789a21a --- /dev/null +++ b/devprogg @@ -0,0 +1,5 @@ +#!/bin/sh + +# Simple wrapper to run vsutil during development. + +ruby -Ilib ./exe/pg-tools "$@" \ No newline at end of file diff --git a/doc/definition.png b/doc/definition.png new file mode 100644 index 0000000..67199d5 Binary files /dev/null and b/doc/definition.png differ diff --git a/doc/diagram.png b/doc/diagram.png new file mode 100644 index 0000000..6aa906e Binary files /dev/null and b/doc/diagram.png differ diff --git a/doc/expose.md b/doc/expose.md new file mode 100644 index 0000000..11fda4c --- /dev/null +++ b/doc/expose.md @@ -0,0 +1,141 @@ +# PG-Tools + +PG-Tools ist ein textasiertes CLI Programm zur Entwicklung und Einbindung von +Programmgraphen im Kontext der formalen Sicherheitsanalyse. + +Ziel ist es, ein anwenderfreundliches, robustes und zukunftssicheres System zu entwickeln, +dass möglichst im Hintergrund bleibt und Platz für das Wesentliche lässt: Das Modellieren. + +## Beispielprojekt + +Damit klarer wird welches System wir uns vorstellen, wird im Folgenden ein kleines +Beispielprojekt vogestellt. Es handelt sich um eine leicht modifizierte Version +des "Weidezaun" projektes aus der Vorlesung. +Die Ausgaben sind teilweise noch von Hand erstellt weil die Implementierung noch +nicht weit genug fortgeschritten ist. d + +### Die Entwicklungsumgebung + +Da wir vorhaben ein CLI Programm zu erstellen, das mit "Plain Text" arbeitet, +ist jede Entwicklungsumgebung denkbar. +Das folgende Bild zeigt also nur ein Beispiel für eine Möglichkeit. +(Mehr dazu [hier](#warum-cli-und-plain-text)) + +![alt text](./definition.png) + +Links auf dem Bild sieht man die definition eines Programmgraphen über die +Ruby DSL. Rechts sieht man die erzeugte Grafik. Die Grafik wird ernuert, sobald +man `pg-tools show` ausführt, so wie unten abgebildet. + +### Validitätsüberprüfungen + +Oben im Bild ist die Definition von Spezifikationen zur Validitätsprüfung. +Führt man `pg-tools test` aus, erhält man die unten dargestellte Ausgabe. +(Das Feature ist noch nicht implementiert. Tatsächlich wären hier einige tests fehlgeschlagen.) +Die Syntax ist vom beliebten Test-Framework [Rspec](https://rspec.info/) inspiriert. +Im Fehlerfall würde der Ablauf ausgegeben, der die Formel verletzt. + +Nach der Fehlerintegration könntem man Fehler beispielsweise so ausschließen: + +```ruby +BEP = 150 +errors = [ :BreaksError, :SensorError ] +# ... +no_errors = errors.map { |error| "G #{error} == no" }.join(" && ") +specify "The train" do + assuming "there are no errors" => no_errors do + it "reaches BEP" => :"G Tain.position > #{BEP}" + end +end +``` + +Zudem könnte man die Ruby DSL so erweitern, dass Fehlerautomaten +im internen Datenmodell von gewöhnlichen Komponenten unterschieden werden können. +Damit könnte man eine knappe Syntax anbieten und die DCCA vollautomaitsch durchführen: + +```ruby +# Erzeugt Fehlerautomaten für die Bremse & den Zugsensor +persistent error :Breaks +transient error :Sensor + +# Validität unter Ausschluss von Fehlern +# 'no_erros' kann hier automatisch generiert wrden +specify "The train" do + assuming "there are no errors" => no_errors do + it "reaches BEP" => :"G Tain.position > #{BEP}" + end +end + +# Definition einer Gefährdung für die DCCA. Ausführbar mit: 'pg-tools dcca' +hazard "Train on unsecured railroad crossing" \ + => :"Barrier.angle > #{barrier_closed_angle} && Train.position >= #{train_pos_gep} && Train.position <= #{tain_pos_sp}" +``` + +# Features + +Im Folgenden einige Ideen für Features: + +- Einlesen von Modellen über Ruby-DSL, Json und Yaml +- Ausgeben von Modellen in Json, Yaml, PlantUML +- Integration von NuSMV, Prism und weiterer model checker. +- Simulation von Modellen und Ausgabe als video/gif +- Integriertes Test-Framework zur Validitätsprüfung +- Deklarative syntax zur Verwendung der "LTL-Pattern" aus der Vorlesung +- Automatische DCCA +- Installation über ein Kommando (`gem install pg-tools`) +- Einfache Einarbeitung (mit Kommando `pg-tools init`) +- Ansprechende Dokumentation +- Konfigurationsmöglichkeiten +- Hilfreiche Fehlermeldungen + +# Warum CLI und Plain Text + +Das Verständnis eines Systems ist zwar die Grundlage der Modellierung, aber nur ihr Anfang. +Erst durch die Konzeptualisierung, ist es möglich Modelle festzuhalten, zu kommunizieren, +Denkfehler aufzudecken und sie maschinell zu verarbeiten. + +Mit den folgenden Argumenten wollen wir Darstellen, warum die Verwendung von "Plain Text" und eines CLI Programms +für die Konzeptualisierung/Festschreibung von Modellen besser geeignet ist, als eine Graphische +Lösung. +(Mit "Pain Text" meinen wir den Ansatz, dass alle Projektdateien ausschließlich Text enthaten, +der schon für sich und ohne die Verwendung von Tools verständlich ist) + +## Unkomplizierte Eingabe + +Graphischen Darstellungen sind sehr nützlich um Modelle zu verstehen. +Dabei liegt ihr Vorteil aber in der Effizienten *Aufnahme* von Informationen, +durch den Betrachter. + +Bei der *Ausgabe* der eignenen Gedanken können graphische Editoren oft hinderlich sein. +Nebensächlichkeiten, wie das Layout und eine umständliche Navigation im UI +stehen dem eigentlichen Ziel, der Modellierung, eher im Weg. + +Wir wollen die Verständlichkeit einer graphischen Ausgabe, +mit der unkomplizierten Eingabe über Text verbinden. + +## Einfache Zusammenarbeit + +Tools wie Git(-hub) sind auf die verarbeitung von Text ausgelegt. +Versionskontrolle, code reviews und das Beheben von merge Konflikten +funktionieren deutlich besser mit "Plain Text". + +## Zeitlosigkeit & Technologie unabhängigkeit + +Die Wartung und Instandhaltung von von UI-basierten Programmen ist nur mit Großem Aufwand möglich. +Bibliotheken veralten und Design trends ändern sich. Während Programme wie Eclipse schlecht gealtert sind, +erfreuen sich command line tools wie "git" oder "make" weiterhin großer Beliebtheit. + +Trotz des Aufkommens neuer Technologien stellen CLI Programme und und die Verwendung von +Plain Text eine Konstante dar. + +## Einfache Installation + +Die Leichtgewichtigkeit eines CLI Programms vereinfacht die Installation und lässt weniger +Spielraum für Fehler. Durch minimale Abhängigkeiten kann die Funktionalität +auf verschiednen systemen sichergestellt werden. + +## Automatisierung und Flexibilität + +CLI programme können einfach in Arbeitsabläufe eingebunden werden. +Beispielsweise wäre es möglich tests für Modelle zu schreiben, die mittles "continuous integration" +für jedem Pull Request auf Github ausgeführt werden. diff --git a/doc/validiy.png b/doc/validiy.png new file mode 100644 index 0000000..2d248d8 Binary files /dev/null and b/doc/validiy.png differ diff --git a/doc/weidezaun.rb b/doc/weidezaun.rb new file mode 100644 index 0000000..59a005f --- /dev/null +++ b/doc/weidezaun.rb @@ -0,0 +1,99 @@ +#################################################################### +# Model definition +#################################################################### + +# Define a component called 'Hand'. +component :Hand do + # The hand can be touching the fence or be somewhere else + # It starts in 'somewhere' as that state is listed first + states :somewhere, :at_fence + + # Transition non-deterministically between those states + transition :somewhere => :somewhere + transition :somewhere => :at_fence + transition :at_fence => :somewhere + transition :at_fence => :at_fence +end + +# Define another component called 'PowerSwitch', which also +# transitions non-deterministically. +component :PowerSwitch do + states :off, :on + transition :off => :off + transition :off => :on + transition :on => :off + transition :on => :on +end + +component :Fence do + # The fence has no states we are interested in + states :exists + + # The fence has a voltage which can go up to 15 + var :voltage => (0..15), init: 0 + + # The voltage increases when the power switch is on + transition :exists => :exists do + guard "PowerSwitch == on" + action "voltage := voltage + 1" + end + # ..and instantly stops when the switch is off + transition :exists => :exists do + guard "PowerSwitch == off" + action "voltage := 0" + end + +end + +component :Pain do + # We can either be in pain or not + states :No, :Yes + # Using regular variables with string interpolation + pain_threshold = 7 + transition :No => :Yes do + guard "Hand == at_fence && voltage >= #{pain_threshold}" + end + transition :Yes => :No do + guard "Hand == somewhere || voltage < #{pain_threshold}" + end +end + +#################################################################### +# Validity tests +#################################################################### + +# Specification of validity characteristics regarding the hand. +# The 'specify' block serves as a namespace/container for the contained specifications +specify "The Hand" do + # Define some simple specs using a description text and an LTL expression + it "isn't always touching the fence" => :"F Hand == somewhere" + it "isn't always away form the fence" => :"F Hand == at_fence" +end + +# Specification of validity characteristics regarding the pain +specify "The pain" do + # Use a regular LTL Formula as the expression + it "is felt at some point" => :"F Pain == yes" + # Use a more declarative syntax. This becomes useful for complex expressions + # as LTL patterns can be used very easily + it "is always felt at some point" => ltl.globally.exists(:"Pain == yes") + + # Pattern: 'Universality', range: 'after q' + it "is felt after the switch is activated" => ltl.after(:"PowerSwitch == on").exists(:"Pain == yes") + # Pattern: 'Absence', range: 'before q' + it "is never felt before the switch is activated" => ltl.before(:"PowerSwitch == on").never(:"Pain == yes") + # Pattern: 'Reaction', range: 'global' + it "always reacts to the switch being activated" => ltl.globally.reacts(:"PowerSwitch == on", :"Pain == yes") + + # Define an assumption. That assumption must be true for all contained specs + assuming "the switch is never activated" => :"G PowerSwitch == off" do + it "is never felt " => :"G Pain == no" + end + + # Assumptions can be nested and used with the declarative syntax. + assuming "the switch is activated" => ltl.globally.exists(:"PowerSwitch == on") do + assuming "the hand never touches the fence" => :"G Hand != at_fence" do + it "is never felt " => :"G Pain == no" + end + end +end diff --git a/exe/pg-tools b/exe/pg-tools new file mode 100755 index 0000000..17d31c2 --- /dev/null +++ b/exe/pg-tools @@ -0,0 +1,4 @@ +#!/usr/bin/env ruby +require_relative '../bin/progg.rb' + +Progg::ProggCLI.new.run() diff --git a/lib/progg.rb b/lib/progg.rb new file mode 100644 index 0000000..579361a --- /dev/null +++ b/lib/progg.rb @@ -0,0 +1,33 @@ +# frozen_string_literal: true + +require_relative "progg/version" +require_relative "progg/core/core.rb" +require_relative "progg/ebnf_parser/ebnf_parser.rb" +require_relative "progg/model/model.rb" +require_relative "progg/interpret/interpret.rb" +require_relative "progg/cli/cli.rb" +require_relative "progg/transform/transform.rb" +require_relative "progg/nusmv/nusmv.rb" +require 'config' +require 'fileutils' + +module Progg + + def self.init() + config_paths = [] + config_paths << File.expand_path('data/config/progg.yml', self.root) + config_paths << File.expand_path('.progg.yml', Dir.home) + config_paths << File.expand_path('.progg.yml', Dir.pwd) + config_paths.select! { |path| File.file?(path) } + Config.load_and_set_settings(*config_paths) + + Colorizer.attach(Settings.colors.to_h) + end + + def self.root() + File.expand_path(File.join(__dir__, "..")) + end + +end + +Progg.init() diff --git a/lib/progg/cli/cli.rb b/lib/progg/cli/cli.rb new file mode 100644 index 0000000..8691c0a --- /dev/null +++ b/lib/progg/cli/cli.rb @@ -0,0 +1,67 @@ +# Require all module files +Dir[File.join(__dir__, '*.rb')].sort.each { |file| require file } + +require 'thor' +require 'plantuml_builder' + +module Progg + module Cli + + class BaseCommand < Thor + + desc "test", "Shows the ProgramGraph" + def test() + + script = Interpret::ProggScript.new + model = script.interpret('program-graph.rb') + + model.specification.flat_specs() + + end + + desc "show", "Shows the ProgramGraph" + option :yell, :type => :boolean + def show() + + puts options[:yell] + + # parser = EbnfParser::ExpressionParser2.new(type: :Sum) + # puts parser.parse!("1 + 2").map + # return + + script = Interpret::ProggScript.new + model = script.interpret('program-graph.rb') + + puml = Tranform::PumlTransformation.new.transform_graph(model) + png = PlantumlBuilder::Formats::PNG.new(puml).load + File.binwrite("diagram.png", png) + + return + + nusmv_t = Tranform::NuSmvTransformation.new + nusmv_s = nusmv_t.transform_graph(model) + + puts "Validating Model..." + errors = model.validate() + puts errors.map(&:to_s).join("\n\n") + + nusmv_file = File.expand_path('nusmv.tmp', Settings.workdir) + FileUtils.mkdir_p(File.dirname(nusmv_file)) + File.write(nusmv_file, nusmv_s) + nurunner = NuSMV::NuSMVRunner.new() + nurunner.load_file(nusmv_file) + + return + + + desc_str = model.specs.map(&:text).join("\n") + expr_str = model.specs.map(&:expression).map(&:to_s).join("\n") + puts desc_str.line_combine(expr_str) + + # + end + + end + + end +end \ No newline at end of file diff --git a/lib/progg/cli/command_executor.rb b/lib/progg/cli/command_executor.rb new file mode 100644 index 0000000..7c93073 --- /dev/null +++ b/lib/progg/cli/command_executor.rb @@ -0,0 +1,42 @@ + + +module Progg + + module Cli + + class CommandExecutor + + RegisteredCommand = Struct.new(:file_path, :path) + + def initialize() + end + + def exec(argv) + cmd = find_command(argv) + end + + def find_command(argv) + cmds = registered_commands() + current_path = [] + argv.each { |word| + current_path << word + candidates = cmds.select { |c| } + } + end + + def registered_commands() + cmds = nil + Dir.chdir(File.join(__dir__, 'commands')) { + cmds = Dir[File.join('.', '**', '*.rb')].map { |file| + next unless File.file?(file) + path = file.gsub('.rb', '').split(File::Separator).reject { |p| p == '.' } + RegisteredCommand.new(file, path) + }.compact + } + return cmds + end + + end + end + +end \ No newline at end of file diff --git a/lib/progg/cli/commands/show.rb b/lib/progg/cli/commands/show.rb new file mode 100644 index 0000000..eb5b1bd --- /dev/null +++ b/lib/progg/cli/commands/show.rb @@ -0,0 +1,15 @@ + + +module Progg + module Cli + + class Show + + + + + + + end + end +end \ No newline at end of file diff --git a/lib/progg/core/core.rb b/lib/progg/core/core.rb new file mode 100644 index 0000000..4e4f3fb --- /dev/null +++ b/lib/progg/core/core.rb @@ -0,0 +1,13 @@ + +# Require all module files +Dir[File.join(__dir__, "**", '*.rb')].sort.each { |file| require file } + +module Progg + + module Core + + class Error < StandardError; end + + end + +end \ No newline at end of file diff --git a/lib/progg/core/extensions/string_extensions.rb b/lib/progg/core/extensions/string_extensions.rb new file mode 100644 index 0000000..79e33ab --- /dev/null +++ b/lib/progg/core/extensions/string_extensions.rb @@ -0,0 +1,84 @@ +class String + + def integer? + self.to_i.to_s == self + end + + def snake_case + self.strip() + .gsub(/ +/, "_") + .gsub(/::/, '/') + .gsub(/([A-Z]+)([A-Z][a-z])/,'\1_\2') + .gsub(/([a-z\d])([A-Z])/,'\1_\2') + .tr("-", "_") + .downcase() + end + + def camel_case + return self if self !~ /_/ && self =~ /[A-Z]+.*/ + split('_').map{|e| e.capitalize}.join + end + + def grep(str, e) + self.split("\n").select { |l| l.include?(str) } + end + + def display_length() + str = Progg::Colorizer.uncolorize(self) + str.length() + ( str.count("\t") * 4 ) + end + + def line_combine(other, separator: " ") + Progg::StringUtil.line_combine(self, other, separator: separator) + end + + def indented(num: 1, str: " " * 4) + Progg::StringUtil.indented(self, num_indents: num, indent_string: str) + end + + def remove_before(substring) + split = self.split(substring) + return "" if split.length == 1 + return split[1, split.length].join(substring) + end + + def blank? + self.empty? + end + + def limit_lines(num_lines, separator: "...") + return "" if num_lines == 0 + split = self.split("\n") + return self unless split.length > num_lines + first_part = split[0, num_lines / 2] + second_part = split[split.length - (num_lines - first_part.length), split.length] + return first_part.join("\n") + "\n#{separator}\n" + second_part.join("\n") + end + + def shorten(length) + return self if self.length <= length + return self[0, [length - 3, 1].max] + "..." + end + + def labelize(bg: :darkgreen, fg: :white) + "◖".send(:"c_#{bg}") + " #{self} ".send(:"bg_#{bg}").send(:"c_#{fg}").c_bold + "◗".send(:"c_#{bg}") + end + + def file?() + File.file?(self) + end + + def directory?() + File.directory?(self) + end + + # Support this method for Ruby <= 2.3 + unless self.method_defined?(:delete_prefix) + def delete_prefix(prefix) + self.respond_to?(:delete_prefix) + return unless self.start_with?(prefix) + return self[prefix.length, self.length - 1] + end + end + +end diff --git a/lib/progg/core/shell/colorizer.rb b/lib/progg/core/shell/colorizer.rb new file mode 100644 index 0000000..4353e6d --- /dev/null +++ b/lib/progg/core/shell/colorizer.rb @@ -0,0 +1,136 @@ +require "rainbow" + +module Progg + + # A Module for easy coloration of strings with theme support. + # After #attach is called strings can be colored using one of any c_ or bg_ methods + # e.g: "Hello".c_cyan, "Hello".bg_blue + # Calls can also by chained: + # e.g: "Hello".c_red.bg_blue.c_bold + # + # A theme is a hash of keys to values. Values can be: + # 1. Hex values. e.g '#00AABB' + # 2. Color names that are defined elswhere. e.g: 'red' + # 3. Arrays of values. e.g [ 'white', '_#000000', 'bold' ] + # If a value starts with an underscore (e.g _red) the color will + # be used as the background color. + # Strings can then be colored using the c_ method. + # e.g: mycolor => [ "#FFFFFF", "_black" ] + # mystyle => [ "mycolor", "bold" ] + # "Hello".c_mystyle <- Colored white on black in bold + module Colorizer + + def self.send_call(rainbow, color_expr) + prefix = color_expr.start_with?("_") ? "bg" : "c" + color_expr = color_expr.sub("_", "") + + # If the color expression is a HEX (e.g #FF3400) .. + if color_expr.start_with?("#") + # Send the call directly to Rainbow + return rainbow.send(prefix == "bg" ? :background : :color, color_expr) + else + # Otherwise forward the call + return rainbow.send("#{prefix}_#{color_expr}".to_sym) + end + end + + def self.define_methods(hash) + Rainbow::X11ColorNames::NAMES.each do |color_name, _| + define_method "c_#{color_name}".to_sym do + Rainbow(self).color(color_name.to_sym) + end + define_method "bg_#{color_name}".to_sym do + Rainbow(self).send(:background, color_name) + end + end + + hash.each do |key, color_names| + array = color_names.is_a?(Array) ? color_names : [ color_names ] + define_method "c_#{key}".to_sym do + rainbow = Rainbow(self) + array.each { |color_name| + rainbow = Colorizer.send_call(rainbow, color_name) + } + rainbow + end + define_method "bg_#{key}".to_sym do + rainbow = Rainbow(self) + array.each { |color_name| + rainbow = Colorizer.send_call(rainbow, "_#{color_name}") + } + rainbow + end + end + end + + def self.uncolorize(string) + string.gsub(/\e\[([;\d]+)?m/, '') + end + + def self.color?(string) + !!/\e\[([;\d]+)?m/.match(string) + end + + def color(color) + method = "c_#{color}".to_sym + return self unless self.respond_to?(method) + self.send(method) + end + + def c_bold + Rainbow(self).bold + end + + def c_italic + Rainbow(self).italic + end + + def c_underline + Rainbow(self).underline + end + + def c_none + self + end + + def color_bg(color) + Rainbow(self).background(color) + end + + def color_regex(hash) + hash.each do |key, val| + self.gsub!(Regexp.new(key)) { |match| + "#{match.color(val)}" + } + end + self + end + + def color_unique() + r, g, b = Colorizer.unique_color(self) + return Rainbow(self).color(r, g, b) + end + + def bg_color_unique() + r, g, b = Colorizer.unique_color(self) + return Rainbow(self).background(r, g, b) + end + + # def self.unique_color(string) + # r = Random.new(Integer("0x#{Digest::SHA256.hexdigest(string)}")) + # number = r.rand(0..360) + # r, g, b = VsuColorUtil.hsl_to_rgb(number, 60, 50) + # return r, g, b + # end + + def self.attach(theme, use_colors: true) + define_methods(theme) + use_colors = Settings.use_colors + use_colors &&= Settings.use_colors_in_pipe if !$stdout.isatty + Rainbow.enabled = use_colors + String.class_eval { include Progg::Colorizer } + end + + end + +end \ No newline at end of file diff --git a/lib/progg/core/util.rb b/lib/progg/core/util.rb new file mode 100644 index 0000000..4fb0e94 --- /dev/null +++ b/lib/progg/core/util.rb @@ -0,0 +1,96 @@ +module Progg + + class StringUtil + + def self.make_unique(string, strings, &blk) + base_string = string + index = 0 + while strings.include?(string) + index += 1 + string = blk.call(base_string, index) + end + string + end + + def self.limit_width(string, width) + return string if string.nil? || string.length <= width + return string.chars.each_slice(width).map(&:join).join("\n") + end + + def self.auto_complete(string, options) + perfect_match = options.select { |o| o == string }.uniq + return perfect_match unless perfect_match.empty? + options.select { |o| o.start_with?(string) }.uniq + end + + def self.levenshtein_suggest(string, options, suggestions: 5) + options.map { |o| [o, levenshtein_distance(string, o)] } + .sort_by{ |a| a[1] } + .vsu_limit(suggestions) + .map { |a| a[0] } + end + + def self.line_combine(string1, string2, separator: " ") + return string2 if string1.empty? + lines1, lines2 = string1.split("\n"), string2.split("\n") + both = [lines1, lines2] + height = both.map(&:length).max + l_width = lines1.map(&:display_length).max + + # Fill up empty lines to match height + both.each { |lines| loop { break if lines.length >= height; lines << "" } } + + # Fill up left lines to align right side + lines1 = lines1.map { |l| l + " " * (l_width - l.display_length) } + + # Combine left and right. + string = (0...height).map { |index| + lines1[index] + separator + lines2[index] + }.join("\n") + + return string + end + + def self.shorten_unique(strings) + # TODO: Implement + return strings.each_with_index.map { |s, i| [s, i.to_s] }.to_h + + # chars = ".- _".chars + # regex = /#{chars.map { |c| "\\#{c}" }.join("|")}/ + # map = {} + # strings.each do |str| + # index = 0 + # loop do + # split = str.gsub(regex, " ").split + # short = split.map { |word| word[0, index] }.join("") + # puts short + # sleep(1) + # next if map.values.include?(short) + # map[str] = short + # break + # end + + # end + + # map + end + + def self.indented(string, num_indents: 1, indent_string: "\t") + string.split("\n").map { |l| "#{indent_string * num_indents}#{l}" }.join("\n") + end + + def self.levenshtein_distance(a, b) + a, b = a.downcase, b.downcase + costs = Array(0..b.length) # i == 0 + (1..a.length).each do |i| + costs[0], nw = i, i - 1 # j == 0; nw is lev(i-1, j) + (1..b.length).each do |j| + costs[j], nw = [costs[j] + 1, costs[j-1] + 1, a[i-1] == b[j-1] ? nw : nw + 1].min, costs[j] + end + end + costs[b.length] + end + + end + +end \ No newline at end of file diff --git a/lib/progg/ebnf_parser/ast.rb b/lib/progg/ebnf_parser/ast.rb new file mode 100644 index 0000000..b7319fd --- /dev/null +++ b/lib/progg/ebnf_parser/ast.rb @@ -0,0 +1,31 @@ +module Progg + module EbnfParser + + class Ast + + attr_accessor :map + + def initialize(map) + @map = map + end + + def find_variables(element=@map) + # TODO: Actually parse the variables + # puts "REC #{element.class}: #{element}" + # puts "\n" + # ret = [] + # ret += element.map { |val| find_variables(val) }.flatten if element.is_a?(Array) + # element.each { |key, value| + # # We found a variable if we found a value which is not a number nor a boolean constant + # if key == :Value && value.is_a?(String) && !(/\d+/.match?(value)) && value != 'true' && value != 'false' + # ret << value + # end + # ret += find_variables(value) + # } if element.is_a?(Hash) + # return ret + end + + end + + end +end \ No newline at end of file diff --git a/lib/progg/ebnf_parser/ebnf_parser.rb b/lib/progg/ebnf_parser/ebnf_parser.rb new file mode 100644 index 0000000..04ab18b --- /dev/null +++ b/lib/progg/ebnf_parser/ebnf_parser.rb @@ -0,0 +1,26 @@ +require 'ebnf' +require 'ebnf/terminals' +require 'ebnf/peg/parser' +require 'sxp' +require 'logger' +require 'json' + +# Require all module files +Dir[File.join(__dir__, "**", '*.rb')].sort.each { |file| require file } + +module Progg + module EbnfParser + + def self.parse_expression(expression, type: :Expression) + parser = ExpressionParser.new(type: type) + error, ast = nil, nil + begin + ast = parser.parse!(expression) + rescue EBNF::PEG::Parser::Error => e + error = e + end + return ParserResult.new(ast, error) + end + + end +end diff --git a/lib/progg/ebnf_parser/expression_parser.rb b/lib/progg/ebnf_parser/expression_parser.rb new file mode 100644 index 0000000..ae0ff16 --- /dev/null +++ b/lib/progg/ebnf_parser/expression_parser.rb @@ -0,0 +1,177 @@ +module Progg + module EbnfParser + + class ExpressionParser + include EBNF::PEG::Parser + + # Abstract syntax tree from parse + attr_reader :ast + attr_accessor :rules + attr_accessor :options + attr_accessor :type + + + # production(:Assignment, clear_packrat: true) do |value| + # # puts"Assignment:".ljust(25) + " #{value}" + # value + # end + + # production(:BoolExpr, clear_packrat: true) do |value| + # # puts"BoolExpr:".ljust(25) + " #{value}" + # value + # end + + # production(:Equivalence, clear_packrat: true) do |value| + # # puts"Equivalence:".ljust(25) + " #{value}" + # value + # end + + # production(:Implication, clear_packrat: true) do |value| + # # puts"Implication:".ljust(25) + " #{value}" + # value + # end + + # production(:Disjunction, clear_packrat: true) do |value| + # # puts"Disjunction:".ljust(25) + " #{value}" + # value + # end + + # production(:Konjunction, clear_packrat: true) do |value| + # # puts"Konjunction:".ljust(25) + " #{value}" + # value + # end + + # production(:Negation, clear_packrat: true) do |value| + # puts"Negation:".ljust(25) + "#{value.class} #{value}" + # value + # end + + # production(:Comparison, clear_packrat: true) do |value| + # # puts"Comparison:".ljust(25) + " #{value}" + # value + # end + + # production(:IntExpr, clear_packrat: true) do |value| + # # puts"IntExpr:".ljust(25) + " #{value}" + # value + # end + + # production(:Sum, clear_packrat: true) do |value| + # # puts"Sum:".ljust(25) + " #{value}" + # value + # end + + # production(:Product, clear_packrat: true) do |value| + # # puts"Product:".ljust(25) + " #{value}" + # valuex + # end + + + + # [{:Value=>"3"}, {:_Product_1=>"* 5 * 5"}] + production(:Product) do |value| + val = value.first[:Value] + prod1 = value.last[:_Product_1] + ret = "#{val} #{prod1}" + puts"Product:".ljust(25) + " #{value} -> #{ret}" + ret + end + + # A list of product operations plus values ['+ 4', '+ 4'] + production(:_Product_1) do |value| + ret = value.join(' ') + # puts"Product1:".ljust(25) + " #{value} -> #{ret}" + ret + end + + # A product operation plus value '+ 4' + production(:_Product_2) do |value| + op = value.first[:_Product_3] + val = value.last[:Value] + ret = "#{op} #{val}" + puts "Product2:".ljust(25) + " #{value} -> #{ret}" + ret + end + + # A product operation '*' '/' + production(:_Product_3) do |value| + operation = value + value + end + + # An atomic value like '3', 'true' or 'variable' + production(:Value) do |value| + value + end + # An expression in braces + production(:_Value_1) do |value| + value.is_a?(Hash) ? value[:Expression] : value + end + # A number like '42' or '-7' + production(:NUMBER) do |value| + value + end + # A boolean value like 'true' or 'false' + production(:BOOL) do |value| + value + end + # A boolean expression in braces like '(3 < 2 <-> true)' + production(:_BOOL_1) do |value| + value.is_a?(Hash) ? value[:BoolExpr] : value + value + end + # Integer comparison operators like '>' and '!=' + production(:CMPOP) do |value| + value + end + + + def initialize(type: :Expression) + @type = type + @options = {} + # @options[:logger] = Logger.new(STDERR) + # @options[:logger].level = :info + # @options[:logger].formatter = lambda {|severity, datetime, progname, msg| "#{severity} #{msg}\n"} + + # Intantiate the grammar + ebnf_file = File.expand_path("expressions.ebnf", __dir__) + # Perform PEG-specific transformation to the associated rules, which will be passed directly to the parser. + @rules = EBNF.parse(File.open(ebnf_file)).make_peg.ast + + skeletton = EBNF.parse(File.open(ebnf_file)).make_peg.to_s.split("\n").reverse.map { |line| + rule = line.split(/\s+/)[1] + comment = "# Rule: '#{line.split(/\s+/).join(" ")}'" + puts_line = 'puts "' + rule + ': \'#{input}\' -> \'#{output}\'"' + body = "\toutput = input\n\t#{puts_line}\n\toutput" + method = "production(:#{rule}) do |input|\n#{body}\nend" + [comment, method].join("\n") + }.join("\n\n") + File.write(File.expand_path("expressions.rb", __dir__), skeletton) + + # TODO: Remove + File.write(File.expand_path("expressions.peg", __dir__), EBNF.parse(File.open(ebnf_file)).make_peg) + end + + def parse!(input) + raise "Empty expression!" if input.nil? || input.empty? + ast_map = parse(input, @type, @rules, **@options) + Ast.new(ast_map) + end + + # def evaluate!(input, type: :Expression) + # # TODO: Change this to actually eval (Also in specs) + # parse(input, type, @rules, **@options) + # end + + # def accepts?(input, type: :Expression) + # begin + # evaluate!(input, type: type) + # return true + # rescue EBNF::PEG::Parser::Error => e + # return false + # end + # end + end + + end +end \ No newline at end of file diff --git a/lib/progg/ebnf_parser/expression_parser2.rb b/lib/progg/ebnf_parser/expression_parser2.rb new file mode 100644 index 0000000..83497f5 --- /dev/null +++ b/lib/progg/ebnf_parser/expression_parser2.rb @@ -0,0 +1,422 @@ +module Progg + module EbnfParser + + class ExpressionParser2 + include EBNF::PEG::Parser + + # Abstract syntax tree from parse + attr_reader :ast + attr_accessor :rules + attr_accessor :options + attr_accessor :type + + # Rule: '[20] CMPOP ::= "<=" | ">=" | "<" | ">" | "==" | "!="' + production(:CMPOP) do |input| + output = input + puts "CMPOP: '#{input}' -> '#{output}'" + output + end + + # Rule: '[19.2] _VARIABLE_2 ::= [a-zA-Z_]' + production(:_VARIABLE_2) do |input| + output = input + puts "_VARIABLE_2: '#{input}' -> '#{output}'" + output + end + + # Rule: '[19.6] _VARIABLE_6 ::= [a-zA-Z0-9_]' + production(:_VARIABLE_6) do |input| + output = input + puts "_VARIABLE_6: '#{input}' -> '#{output}'" + output + end + + # Rule: '[19.5] _VARIABLE_5 ::= _VARIABLE_6*' + production(:_VARIABLE_5) do |input| + output = input + puts "_VARIABLE_5: '#{input}' -> '#{output}'" + output + end + + # Rule: '[19.4] _VARIABLE_4 ::= [a-zA-Z_]' + production(:_VARIABLE_4) do |input| + output = input + puts "_VARIABLE_4: '#{input}' -> '#{output}'" + output + end + + # Rule: '[19.3] _VARIABLE_3 ::= [^('true'#x20|#x20'false')]' + production(:_VARIABLE_3) do |input| + output = input + puts "_VARIABLE_3: '#{input}' -> '#{output}'" + output + end + + # Rule: '[19.1] _VARIABLE_1 ::= _VARIABLE_3 _VARIABLE_4 _VARIABLE_5' + production(:_VARIABLE_1) do |input| + output = input + puts "_VARIABLE_1: '#{input}' -> '#{output}'" + output + end + + # Rule: '[19] VARIABLE ::= _VARIABLE_1 | _VARIABLE_2' + production(:VARIABLE) do |input| + output = input + puts "VARIABLE: '#{input}' -> '#{output}'" + output + end + + # Rule: '[18.1] _BOOL_1 ::= "(" BoolExpr ")"' + production(:_BOOL_1) do |input| + output = input + puts "_BOOL_1: '#{input}' -> '#{output}'" + output + end + + # Rule: '[18] BOOL ::= "true" | "false" | _BOOL_1' + production(:BOOL) do |input| + output = input + puts "BOOL: '#{input}' -> '#{output}'" + output + end + + # Rule: '[17.3] _NUMBER_3 ::= [0-9]' + production(:_NUMBER_3) do |input| + output = input + puts "_NUMBER_3: '#{input}' -> '#{output}'" + output + end + + # Rule: '[17.2] _NUMBER_2 ::= _NUMBER_3+' + production(:_NUMBER_2) do |input| + output = input + puts "_NUMBER_2: '#{input}' -> '#{output}'" + output + end + + # Rule: '[17.1] _NUMBER_1 ::= "-"?' + production(:_NUMBER_1) do |input| + output = input + puts "_NUMBER_1: '#{input}' -> '#{output}'" + output + end + + # Rule: '[17] NUMBER ::= _NUMBER_1 _NUMBER_2' + production(:NUMBER) do |input| + output = input + puts "NUMBER: '#{input}' -> '#{output}'" + output + end + + # Rule: '[16.1] _Value_1 ::= "(" Expression ")"' + production(:_Value_1) do |input| + output = input + puts "_Value_1: '#{input}' -> '#{output}'" + output + end + + # Rule: '[16] Value ::= NUMBER | VARIABLE | _Value_1' + production(:Value) do |input| + output = input + puts "Value: '#{input}' -> '#{output}'" + output + end + + # Rule: '[15.3] _Product_3 ::= "*" | "/"' + production(:_Product_3) do |input| + output = input + puts "_Product_3: '#{input}' -> '#{output}'" + output + end + + # Rule: '[15.2] _Product_2 ::= _Product_3 Value' + production(:_Product_2) do |input| + operation = input.first[:_Product_3] + value = input.last[:Value] + output = "#{operation} #{value}" + puts "_Product_2: '#{input}' -> '#{output}'" + output + end + + # Rule: '[15.1] _Product_1 ::= _Product_2*' + production(:_Product_1) do |input| + output = input + puts "_Product_1: '#{input}' -> '#{output}'" + output + end + + # Rule: '[15] Product ::= Value _Product_1' + production(:Product) do |input| + value = input.first[:Value] + product_1_results = input.last[:_Product_1] + output = "#{value} #{product_1_results.join(' ')}" + puts "Product: '#{input}' -> '#{output}'" + output + end + + # Rule: '[14.3] _Sum_3 ::= "+" | "-"' + production(:_Sum_3) do |input| + output = input + puts "_Sum_3: '#{input}' -> '#{output}'" + output + end + + # Rule: '[14.2] _Sum_2 ::= _Sum_3 Product' + production(:_Sum_2) do |input| + operation = input.first[:_Sum_3] + value = input.last[:Product] + output = "#{operation} #{value}" + puts "_Sum_2: '#{input}' -> '#{output}'" + output + end + + # Rule: '[14.1] _Sum_1 ::= _Sum_2*' + production(:_Sum_1) do |input| + output = input + puts "_Sum_1: '#{input}' -> '#{output}'" + output + end + + # Rule: '[14] Sum ::= Product _Sum_1' + production(:Sum) do |input| + value = input.first[:Product] + sum_1_results = input.last[:_Sum_1] + output = "#{value} #{sum_1_results.join(' ')}" + puts "Sum: '#{input}' -> '#{output}'" + output + end + + # Rule: '[13] IntExpr ::= Sum' + production(:IntExpr) do |input| + output = input + puts "IntExpr: '#{input}' -> '#{output}'" + output + end + + # Rule: '[12.3] _Comparison_3 ::= CMPOP Sum' + production(:_Comparison_3) do |input| + output = input + puts "_Comparison_3: '#{input}' -> '#{output}'" + output + end + + # Rule: '[12.2] _Comparison_2 ::= _Comparison_3+' + production(:_Comparison_2) do |input| + output = input + puts "_Comparison_2: '#{input}' -> '#{output}'" + output + end + + # Rule: '[12.1] _Comparison_1 ::= Sum _Comparison_2' + production(:_Comparison_1) do |input| + output = input + puts "_Comparison_1: '#{input}' -> '#{output}'" + output + end + + # Rule: '[12] Comparison ::= BOOL | _Comparison_1' + production(:Comparison) do |input| + output = input + puts "Comparison: '#{input}' -> '#{output}'" + output + end + + # Rule: '[11.1] _Negation_1 ::= "!" Comparison' + production(:_Negation_1) do |input| + output = input + puts "_Negation_1: '#{input}' -> '#{output}'" + output + end + + # Rule: '[11] Negation ::= _Negation_1 | Comparison' + production(:Negation) do |input| + output = input + puts "Negation: '#{input}' -> '#{output}'" + output + end + + # Rule: '[10.2] _Konjunction_2 ::= "&&" Negation' + production(:_Konjunction_2) do |input| + output = input + puts "_Konjunction_2: '#{input}' -> '#{output}'" + output + end + + # Rule: '[10.1] _Konjunction_1 ::= _Konjunction_2*' + production(:_Konjunction_1) do |input| + output = input + puts "_Konjunction_1: '#{input}' -> '#{output}'" + output + end + + # Rule: '[10] Konjunction ::= Negation _Konjunction_1' + production(:Konjunction) do |input| + output = input + puts "Konjunction: '#{input}' -> '#{output}'" + output + end + + # Rule: '[9.2] _Disjunction_2 ::= "||" Konjunction' + production(:_Disjunction_2) do |input| + output = input + puts "_Disjunction_2: '#{input}' -> '#{output}'" + output + end + + # Rule: '[9.1] _Disjunction_1 ::= _Disjunction_2*' + production(:_Disjunction_1) do |input| + output = input + puts "_Disjunction_1: '#{input}' -> '#{output}'" + output + end + + # Rule: '[9] Disjunction ::= Konjunction _Disjunction_1' + production(:Disjunction) do |input| + output = input + puts "Disjunction: '#{input}' -> '#{output}'" + output + end + + # Rule: '[8.2] _Implication_2 ::= "->" Disjunction' + production(:_Implication_2) do |input| + output = input + puts "_Implication_2: '#{input}' -> '#{output}'" + output + end + + # Rule: '[8.1] _Implication_1 ::= _Implication_2*' + production(:_Implication_1) do |input| + output = input + puts "_Implication_1: '#{input}' -> '#{output}'" + output + end + + # Rule: '[8] Implication ::= Disjunction _Implication_1' + production(:Implication) do |input| + output = input + puts "Implication: '#{input}' -> '#{output}'" + output + end + + # Rule: '[7.3] _Equivalence_3 ::= "<->" | ""' + production(:_Equivalence_3) do |input| + output = input + puts "_Equivalence_3: '#{input}' -> '#{output}'" + output + end + + # Rule: '[7.2] _Equivalence_2 ::= _Equivalence_3 Implication' + production(:_Equivalence_2) do |input| + output = input + puts "_Equivalence_2: '#{input}' -> '#{output}'" + output + end + + # Rule: '[7.1] _Equivalence_1 ::= _Equivalence_2*' + production(:_Equivalence_1) do |input| + output = input + puts "_Equivalence_1: '#{input}' -> '#{output}'" + output + end + + # Rule: '[7] Equivalence ::= Implication _Equivalence_1' + production(:Equivalence) do |input| + output = input + puts "Equivalence: '#{input}' -> '#{output}'" + output + end + + # Rule: '[6] BoolExpr ::= Equivalence' + production(:BoolExpr) do |input| + output = input + puts "BoolExpr: '#{input}' -> '#{output}'" + output + end + + # Rule: '[5] Expression ::= BoolExpr | IntExpr' + production(:Expression) do |input| + output = input + puts "Expression: '#{input}' -> '#{output}'" + output + end + + # Rule: '[4] Assignment ::= VARIABLE ":=" IntExpr' + production(:Assignment) do |input| + output = input + puts "Assignment: '#{input}' -> '#{output}'" + output + end + + # Rule: '[3] Precon ::= BoolExpr' + production(:Precon) do |input| + output = input + puts "Precon: '#{input}' -> '#{output}'" + output + end + + # Rule: '[2] Guard ::= BoolExpr' + production(:Guard) do |input| + output = input + puts "Guard: '#{input}' -> '#{output}'" + output + end + + # Rule: '[1.2] _Action_2 ::= "|" Assignment' + production(:_Action_2) do |input| + output = input + puts "_Action_2: '#{input}' -> '#{output}'" + output + end + + # Rule: '[1.1] _Action_1 ::= _Action_2*' + production(:_Action_1) do |input| + output = input + puts "_Action_1: '#{input}' -> '#{output}'" + output + end + + # Rule: '[1] Action ::= Assignment _Action_1' + production(:Action) do |input| + output = input + puts "Action: '#{input}' -> '#{output}'" + output + end + + + def initialize(type: :Expression) + @type = type + @options = {} + # @options[:logger] = Logger.new(STDERR) + # @options[:logger].level = :info + # @options[:logger].formatter = lambda {|severity, datetime, progname, msg| "#{severity} #{msg}\n"} + + # Intantiate the grammar + ebnf_file = File.expand_path("expressions.ebnf", __dir__) + # Perform PEG-specific transformation to the associated rules, which will be passed directly to the parser. + @rules = EBNF.parse(File.open(ebnf_file)).make_peg.ast + + end + + def parse!(input) + raise "Empty expression!" if input.nil? || input.empty? + ast_map = parse(input, @type, @rules, **@options) + Ast.new(ast_map) + end + + # def evaluate!(input, type: :Expression) + # # TODO: Change this to actually eval (Also in specs) + # parse(input, type, @rules, **@options) + # end + + # def accepts?(input, type: :Expression) + # begin + # evaluate!(input, type: type) + # return true + # rescue EBNF::PEG::Parser::Error => e + # return false + # end + # end + end + + end +end \ No newline at end of file diff --git a/lib/progg/ebnf_parser/expressions.ebnf b/lib/progg/ebnf_parser/expressions.ebnf new file mode 100644 index 0000000..40cf373 --- /dev/null +++ b/lib/progg/ebnf_parser/expressions.ebnf @@ -0,0 +1,33 @@ +/* + This grammar accepts a combination of + Note that boolean variables are not supported, thus + this expression will be rejected: 'A && true' +*/ + +[1] Action ::= Assignment ('|' Assignment)* +[2] Guard ::= BoolExpr +[3] Precon ::= BoolExpr + +[4] Assignment ::= VARIABLE ':=' IntExpr +[5] Expression ::= BoolExpr | IntExpr + +[6] BoolExpr ::= Equivalence +[7] Equivalence ::= Implication (('<->' | '') Implication)* +[8] Implication ::= Disjunction ('->' Disjunction)* +[9] Disjunction ::= Konjunction ('||' Konjunction)* +[10] Konjunction ::= Negation ('&&' Negation)* +[11] Negation ::= '!' Comparison | Comparison + +[12] Comparison ::= BOOL | Sum (CMPOP Sum)+ + +[13] IntExpr ::= Sum +[14] Sum ::= Product (('+' | '-') Product)* +[15] Product ::= Value (('*' | '/') Value)* +[16] Value ::= NUMBER | VARIABLE | '(' Expression ')' + +[17] NUMBER ::= '-'?[0-9]+ +[18] BOOL ::= 'true' | 'false' | '(' BoolExpr ')' +// Note that we do have to exclude 'true' & 'false' because otherwise 'true' & 'false' +// would be legal Integer expressions as they would be considered variables +[19] VARIABLE ::= [^('true' | 'false')][a-zA-Z_][a-zA-Z0-9_]* | [a-zA-Z_] +[20] CMPOP ::= '<=' | '>=' | '<' | '>' | '==' | '!=' diff --git a/lib/progg/ebnf_parser/expressions.peg b/lib/progg/ebnf_parser/expressions.peg new file mode 100644 index 0000000..413f9ca --- /dev/null +++ b/lib/progg/ebnf_parser/expressions.peg @@ -0,0 +1,52 @@ +[1] Action ::= Assignment _Action_1 +[1.1] _Action_1 ::= _Action_2* +[1.2] _Action_2 ::= "|" Assignment +[2] Guard ::= BoolExpr +[3] Precon ::= BoolExpr +[4] Assignment ::= VARIABLE ":=" IntExpr +[5] Expression ::= BoolExpr | IntExpr +[6] BoolExpr ::= Equivalence +[7] Equivalence ::= Implication _Equivalence_1 +[7.1] _Equivalence_1 ::= _Equivalence_2* +[7.2] _Equivalence_2 ::= _Equivalence_3 Implication +[7.3] _Equivalence_3 ::= "<->" | "" +[8] Implication ::= Disjunction _Implication_1 +[8.1] _Implication_1 ::= _Implication_2* +[8.2] _Implication_2 ::= "->" Disjunction +[9] Disjunction ::= Konjunction _Disjunction_1 +[9.1] _Disjunction_1 ::= _Disjunction_2* +[9.2] _Disjunction_2 ::= "||" Konjunction +[10] Konjunction ::= Negation _Konjunction_1 +[10.1] _Konjunction_1 ::= _Konjunction_2* +[10.2] _Konjunction_2 ::= "&&" Negation +[11] Negation ::= _Negation_1 | Comparison +[11.1] _Negation_1 ::= "!" Comparison +[12] Comparison ::= BOOL | _Comparison_1 +[12.1] _Comparison_1 ::= Sum _Comparison_2 +[12.2] _Comparison_2 ::= _Comparison_3+ +[12.3] _Comparison_3 ::= CMPOP Sum +[13] IntExpr ::= Sum +[14] Sum ::= Product _Sum_1 +[14.1] _Sum_1 ::= _Sum_2* +[14.2] _Sum_2 ::= _Sum_3 Product +[14.3] _Sum_3 ::= "+" | "-" +[15] Product ::= Value _Product_1 +[15.1] _Product_1 ::= _Product_2* +[15.2] _Product_2 ::= _Product_3 Value +[15.3] _Product_3 ::= "*" | "/" +[16] Value ::= NUMBER | VARIABLE | _Value_1 +[16.1] _Value_1 ::= "(" Expression ")" +[17] NUMBER ::= _NUMBER_1 _NUMBER_2 +[17.1] _NUMBER_1 ::= "-"? +[17.2] _NUMBER_2 ::= _NUMBER_3+ +[17.3] _NUMBER_3 ::= [0-9] +[18] BOOL ::= "true" | "false" | _BOOL_1 +[18.1] _BOOL_1 ::= "(" BoolExpr ")" +[19] VARIABLE ::= _VARIABLE_1 | _VARIABLE_2 +[19.1] _VARIABLE_1 ::= _VARIABLE_3 _VARIABLE_4 _VARIABLE_5 +[19.3] _VARIABLE_3 ::= [^('true'#x20|#x20'false')] +[19.4] _VARIABLE_4 ::= [a-zA-Z_] +[19.5] _VARIABLE_5 ::= _VARIABLE_6* +[19.6] _VARIABLE_6 ::= [a-zA-Z0-9_] +[19.2] _VARIABLE_2 ::= [a-zA-Z_] +[20] CMPOP ::= "<=" | ">=" | "<" | ">" | "==" | "!=" diff --git a/lib/progg/ebnf_parser/expressions.rb b/lib/progg/ebnf_parser/expressions.rb new file mode 100644 index 0000000..f47d3d5 --- /dev/null +++ b/lib/progg/ebnf_parser/expressions.rb @@ -0,0 +1,363 @@ +# Rule: '[20] CMPOP ::= "<=" | ">=" | "<" | ">" | "==" | "!="' +production(:CMPOP) do |input| + output = input + puts "CMPOP: '#{input}' -> '#{output}'" + output +end + +# Rule: '[19.2] _VARIABLE_2 ::= [a-zA-Z_]' +production(:_VARIABLE_2) do |input| + output = input + puts "_VARIABLE_2: '#{input}' -> '#{output}'" + output +end + +# Rule: '[19.6] _VARIABLE_6 ::= [a-zA-Z0-9_]' +production(:_VARIABLE_6) do |input| + output = input + puts "_VARIABLE_6: '#{input}' -> '#{output}'" + output +end + +# Rule: '[19.5] _VARIABLE_5 ::= _VARIABLE_6*' +production(:_VARIABLE_5) do |input| + output = input + puts "_VARIABLE_5: '#{input}' -> '#{output}'" + output +end + +# Rule: '[19.4] _VARIABLE_4 ::= [a-zA-Z_]' +production(:_VARIABLE_4) do |input| + output = input + puts "_VARIABLE_4: '#{input}' -> '#{output}'" + output +end + +# Rule: '[19.3] _VARIABLE_3 ::= [^('true'#x20|#x20'false')]' +production(:_VARIABLE_3) do |input| + output = input + puts "_VARIABLE_3: '#{input}' -> '#{output}'" + output +end + +# Rule: '[19.1] _VARIABLE_1 ::= _VARIABLE_3 _VARIABLE_4 _VARIABLE_5' +production(:_VARIABLE_1) do |input| + output = input + puts "_VARIABLE_1: '#{input}' -> '#{output}'" + output +end + +# Rule: '[19] VARIABLE ::= _VARIABLE_1 | _VARIABLE_2' +production(:VARIABLE) do |input| + output = input + puts "VARIABLE: '#{input}' -> '#{output}'" + output +end + +# Rule: '[18.1] _BOOL_1 ::= "(" BoolExpr ")"' +production(:_BOOL_1) do |input| + output = input + puts "_BOOL_1: '#{input}' -> '#{output}'" + output +end + +# Rule: '[18] BOOL ::= "true" | "false" | _BOOL_1' +production(:BOOL) do |input| + output = input + puts "BOOL: '#{input}' -> '#{output}'" + output +end + +# Rule: '[17.3] _NUMBER_3 ::= [0-9]' +production(:_NUMBER_3) do |input| + output = input + puts "_NUMBER_3: '#{input}' -> '#{output}'" + output +end + +# Rule: '[17.2] _NUMBER_2 ::= _NUMBER_3+' +production(:_NUMBER_2) do |input| + output = input + puts "_NUMBER_2: '#{input}' -> '#{output}'" + output +end + +# Rule: '[17.1] _NUMBER_1 ::= "-"?' +production(:_NUMBER_1) do |input| + output = input + puts "_NUMBER_1: '#{input}' -> '#{output}'" + output +end + +# Rule: '[17] NUMBER ::= _NUMBER_1 _NUMBER_2' +production(:NUMBER) do |input| + output = input + puts "NUMBER: '#{input}' -> '#{output}'" + output +end + +# Rule: '[16.1] _Value_1 ::= "(" Expression ")"' +production(:_Value_1) do |input| + output = input + puts "_Value_1: '#{input}' -> '#{output}'" + output +end + +# Rule: '[16] Value ::= NUMBER | VARIABLE | _Value_1' +production(:Value) do |input| + output = input + puts "Value: '#{input}' -> '#{output}'" + output +end + +# Rule: '[15.3] _Product_3 ::= "*" | "/"' +production(:_Product_3) do |input| + output = input + puts "_Product_3: '#{input}' -> '#{output}'" + output +end + +# Rule: '[15.2] _Product_2 ::= _Product_3 Value' +production(:_Product_2) do |input| + output = input + puts "_Product_2: '#{input}' -> '#{output}'" + output +end + +# Rule: '[15.1] _Product_1 ::= _Product_2*' +production(:_Product_1) do |input| + output = input + puts "_Product_1: '#{input}' -> '#{output}'" + output +end + +# Rule: '[15] Product ::= Value _Product_1' +production(:Product) do |input| + output = input + puts "Product: '#{input}' -> '#{output}'" + output +end + +# Rule: '[14.3] _Sum_3 ::= "+" | "-"' +production(:_Sum_3) do |input| + output = input + puts "_Sum_3: '#{input}' -> '#{output}'" + output +end + +# Rule: '[14.2] _Sum_2 ::= _Sum_3 Product' +production(:_Sum_2) do |input| + output = input + puts "_Sum_2: '#{input}' -> '#{output}'" + output +end + +# Rule: '[14.1] _Sum_1 ::= _Sum_2*' +production(:_Sum_1) do |input| + output = input + puts "_Sum_1: '#{input}' -> '#{output}'" + output +end + +# Rule: '[14] Sum ::= Product _Sum_1' +production(:Sum) do |input| + output = input + puts "Sum: '#{input}' -> '#{output}'" + output +end + +# Rule: '[13] IntExpr ::= Sum' +production(:IntExpr) do |input| + output = input + puts "IntExpr: '#{input}' -> '#{output}'" + output +end + +# Rule: '[12.3] _Comparison_3 ::= CMPOP Sum' +production(:_Comparison_3) do |input| + output = input + puts "_Comparison_3: '#{input}' -> '#{output}'" + output +end + +# Rule: '[12.2] _Comparison_2 ::= _Comparison_3+' +production(:_Comparison_2) do |input| + output = input + puts "_Comparison_2: '#{input}' -> '#{output}'" + output +end + +# Rule: '[12.1] _Comparison_1 ::= Sum _Comparison_2' +production(:_Comparison_1) do |input| + output = input + puts "_Comparison_1: '#{input}' -> '#{output}'" + output +end + +# Rule: '[12] Comparison ::= BOOL | _Comparison_1' +production(:Comparison) do |input| + output = input + puts "Comparison: '#{input}' -> '#{output}'" + output +end + +# Rule: '[11.1] _Negation_1 ::= "!" Comparison' +production(:_Negation_1) do |input| + output = input + puts "_Negation_1: '#{input}' -> '#{output}'" + output +end + +# Rule: '[11] Negation ::= _Negation_1 | Comparison' +production(:Negation) do |input| + output = input + puts "Negation: '#{input}' -> '#{output}'" + output +end + +# Rule: '[10.2] _Konjunction_2 ::= "&&" Negation' +production(:_Konjunction_2) do |input| + output = input + puts "_Konjunction_2: '#{input}' -> '#{output}'" + output +end + +# Rule: '[10.1] _Konjunction_1 ::= _Konjunction_2*' +production(:_Konjunction_1) do |input| + output = input + puts "_Konjunction_1: '#{input}' -> '#{output}'" + output +end + +# Rule: '[10] Konjunction ::= Negation _Konjunction_1' +production(:Konjunction) do |input| + output = input + puts "Konjunction: '#{input}' -> '#{output}'" + output +end + +# Rule: '[9.2] _Disjunction_2 ::= "||" Konjunction' +production(:_Disjunction_2) do |input| + output = input + puts "_Disjunction_2: '#{input}' -> '#{output}'" + output +end + +# Rule: '[9.1] _Disjunction_1 ::= _Disjunction_2*' +production(:_Disjunction_1) do |input| + output = input + puts "_Disjunction_1: '#{input}' -> '#{output}'" + output +end + +# Rule: '[9] Disjunction ::= Konjunction _Disjunction_1' +production(:Disjunction) do |input| + output = input + puts "Disjunction: '#{input}' -> '#{output}'" + output +end + +# Rule: '[8.2] _Implication_2 ::= "->" Disjunction' +production(:_Implication_2) do |input| + output = input + puts "_Implication_2: '#{input}' -> '#{output}'" + output +end + +# Rule: '[8.1] _Implication_1 ::= _Implication_2*' +production(:_Implication_1) do |input| + output = input + puts "_Implication_1: '#{input}' -> '#{output}'" + output +end + +# Rule: '[8] Implication ::= Disjunction _Implication_1' +production(:Implication) do |input| + output = input + puts "Implication: '#{input}' -> '#{output}'" + output +end + +# Rule: '[7.3] _Equivalence_3 ::= "<->" | ""' +production(:_Equivalence_3) do |input| + output = input + puts "_Equivalence_3: '#{input}' -> '#{output}'" + output +end + +# Rule: '[7.2] _Equivalence_2 ::= _Equivalence_3 Implication' +production(:_Equivalence_2) do |input| + output = input + puts "_Equivalence_2: '#{input}' -> '#{output}'" + output +end + +# Rule: '[7.1] _Equivalence_1 ::= _Equivalence_2*' +production(:_Equivalence_1) do |input| + output = input + puts "_Equivalence_1: '#{input}' -> '#{output}'" + output +end + +# Rule: '[7] Equivalence ::= Implication _Equivalence_1' +production(:Equivalence) do |input| + output = input + puts "Equivalence: '#{input}' -> '#{output}'" + output +end + +# Rule: '[6] BoolExpr ::= Equivalence' +production(:BoolExpr) do |input| + output = input + puts "BoolExpr: '#{input}' -> '#{output}'" + output +end + +# Rule: '[5] Expression ::= BoolExpr | IntExpr' +production(:Expression) do |input| + output = input + puts "Expression: '#{input}' -> '#{output}'" + output +end + +# Rule: '[4] Assignment ::= VARIABLE ":=" IntExpr' +production(:Assignment) do |input| + output = input + puts "Assignment: '#{input}' -> '#{output}'" + output +end + +# Rule: '[3] Precon ::= BoolExpr' +production(:Precon) do |input| + output = input + puts "Precon: '#{input}' -> '#{output}'" + output +end + +# Rule: '[2] Guard ::= BoolExpr' +production(:Guard) do |input| + output = input + puts "Guard: '#{input}' -> '#{output}'" + output +end + +# Rule: '[1.2] _Action_2 ::= "|" Assignment' +production(:_Action_2) do |input| + output = input + puts "_Action_2: '#{input}' -> '#{output}'" + output +end + +# Rule: '[1.1] _Action_1 ::= _Action_2*' +production(:_Action_1) do |input| + output = input + puts "_Action_1: '#{input}' -> '#{output}'" + output +end + +# Rule: '[1] Action ::= Assignment _Action_1' +production(:Action) do |input| + output = input + puts "Action: '#{input}' -> '#{output}'" + output +end \ No newline at end of file diff --git a/lib/progg/ebnf_parser/parser_result.rb b/lib/progg/ebnf_parser/parser_result.rb new file mode 100644 index 0000000..c7ccc50 --- /dev/null +++ b/lib/progg/ebnf_parser/parser_result.rb @@ -0,0 +1,26 @@ +module Progg + module EbnfParser + + class ParserResult + + attr_accessor :ast + attr_accessor :error + + def initialize(ast, error) + @ast, @error = ast, error + end + + def check!() + return unless error?() + # TODO: Custom exception + raise @error + end + + def error?() + return !@error.nil? + end + + end + + end +end diff --git a/lib/progg/interpret/action_context.rb b/lib/progg/interpret/action_context.rb new file mode 100644 index 0000000..bb204d4 --- /dev/null +++ b/lib/progg/interpret/action_context.rb @@ -0,0 +1,38 @@ +module Progg + module Interpret + + class ActionContext + + attr_accessor :parent_transition + attr_accessor :expression + + def initialize(parent_transition, expression) + @parent_transition = parent_transition + @expression = Model::Expression.new(expression) + raise InterpretError.new("Could not find variable assignment in action '#{@expression}'") if @expression.assigned_variable.nil? + end + + def to_model() + # Resolve the assigned variable + owned_vars = parent_transition.parent_component.variable_list + resolved_assigned_var = owned_vars.detect { |var| var.name == @expression.assigned_variable } + raise "Action '#{@expression}' assigns a value to #{@expression.assigned_variable} " \ + "which isn't owned by the parent component #{parent_transition.parent_component.name}!" if resolved_assigned_var.nil? + + # Resolve variables used in the expression + imported_vars = parent_transition.parent_component.resolve_imported_variables + resolved_imported_vars = @expression.term_variables.map { |varname| + resolved = (owned_vars + imported_vars).detect { |var| var.name == varname } + raise "Action '#{@expression}' uses variable '#{varname}' which could not be resolved." if resolved.nil? + resolved + } + + all_variables = ([ resolved_assigned_var ] + resolved_imported_vars ).uniq + + Model::Action.new(@expression, all_variables) + end + + end + + end +end \ No newline at end of file diff --git a/lib/progg/interpret/component_context.rb b/lib/progg/interpret/component_context.rb new file mode 100644 index 0000000..175882c --- /dev/null +++ b/lib/progg/interpret/component_context.rb @@ -0,0 +1,105 @@ + +module Progg + module Interpret + + class ComponentContext + + # Name of this component as a symbol + attr_accessor :name + + # The list of states of this component as symbols + attr_accessor :states_list + + # The list of transitions of this component + attr_accessor :transition_list + + # The list of variables which is component has declared + # and thus owns + attr_accessor :owned_variables + + # Backreference to the parent graph + attr_accessor :parent_graph + + # A list of variable names to be imported by this component + # attr_accessor :imported_variables + + def initialize(name, parent_graph) + @name, @parent_graph = name, parent_graph + @states_list, @transition_list = [], [] + @owned_variables = [] + # @imported_variables = [] + end + + # DSL method for declaring a variable to be owned by this component + def var(hash) + name = hash.keys.first + range = hash[name] + raise InterpretError.new("Variable name '#{name}' is not a symbol") unless name.is_a?(Symbol) + raise InterpretError.new("Variable range '#{range}' is not a range of integers") unless range.is_a?(Range) && range.first.is_a?(Integer) + variable = Model::Variable.new(name, range, @name) + # puts variable.inspect + variable.initial_value = hash[:init] if hash.key?(:init) + @owned_variables << variable + return variable + end + + # def use(varname) + # @imported_variables << varname + # end + + # DSL method to define states which this component can have + def states(*states) + states.each { |state| + raise InterpretError.new("State '#{state}' is neither a string or symbol") unless state.is_a?(String) || state.is_a?(Symbol) + raise InterpretError.new("State '#{state}' was already declared for component '#{name}'") if @states_list.include?(state) + } + @states_list += states.map(&:to_sym) + end + + # DSL method for the definition of one state + def state(state) + states(state) + end + + # DSL method for the decleration of a transition between states of this component + def transition(hash, &blk) + from = hash.keys.first + to = hash[from] + [ from, to ].each { |state| + raise InterpretError.new("No such state '#{state}' in component '#{name}'") unless @states_list.include?(state) + } + transition = TransitionContext.new(self, from, to) + transition.instance_eval(&blk) unless blk.nil? + @transition_list << transition + return transition + end + + def to_model() + params = {} + # Use the name as is + params[:name] = @name + # Use states as is + params[:states] = @states_list + # Convert the transitions to their model representation + params[:transitions] = @transition_list.map(&:to_model) + + # Create a model component using these params + Model::Component.new(params) + end + + # def resolve_imported_variables() + # other_cmp_vars = @parent_graph.components.map { |cmp| + # next if cmp == self + # cmp.variable_list + # }.compact.flatten + # return @imported_variables.map { |varname| + # var = other_cmp_vars.detect { |var| var.name == varname } + # raise "Can not find variable to import '#{varname}'. Variables: #{other_cmp_vars.map(&:name).join(', ')}" if var.nil? + # var + # } + # end + + end + + end +end \ No newline at end of file diff --git a/lib/progg/interpret/condition_context.rb b/lib/progg/interpret/condition_context.rb new file mode 100644 index 0000000..a8e8cb8 --- /dev/null +++ b/lib/progg/interpret/condition_context.rb @@ -0,0 +1,32 @@ +module Progg + module Interpret + + class ConditionContext + + attr_accessor :parent_transition + attr_accessor :expression + + def initialize(parent_transition, expression) + @parent_transition = parent_transition + @expression = Model::Expression.new(expression) + end + + def to_model() + # Resolve variables used in the expression + owned_vars = parent_transition.parent_component.variable_list + imported_vars = parent_transition.parent_component.resolve_imported_variables + resolved_imported_vars = @expression.term_variables.map { |varname| + resolved = (owned_vars + imported_vars).detect { |var| var.name == varname } + raise "Condition '#{@expression}' uses variable '#{varname}' which could not be resolved." if resolved.nil? + resolved + } + + all_variables = resolved_imported_vars.uniq + + Model::Condition.new(@expression, all_variables) + end + + end + + end +end \ No newline at end of file diff --git a/lib/progg/interpret/graph_context.rb b/lib/progg/interpret/graph_context.rb new file mode 100644 index 0000000..76070a8 --- /dev/null +++ b/lib/progg/interpret/graph_context.rb @@ -0,0 +1,46 @@ + +module Progg + module Interpret + + class GraphContext + + # The list of currently declared components + attr_accessor :components + + attr_accessor :specs + + def initialize() + @components = [] + @specs = [] + end + + # DSL method for declaring a new component in this graph + def component(name, &blk) + cmp = ComponentContext.new(name, self) + cmp.instance_eval(&blk) + @components << cmp + return cmp + end + + # DSL method for declaring a new specification in this graph + def specify(text, &blk) + specset = SpecSetContext.new(text, nil) + specset.instance_eval(&blk) + @specs << specset + end + + def to_model() + components = @components.map(&:to_model) + variables = Model::VariableSet.new(*@components.map(&:owned_variables).flatten()) + specification = Model::Specification.new(@specs.map { |s| s.to_model(nil) }) + Model::Graph.new(components: components, variables: variables, specification: specification) + end + + def get_binding() + binding() + end + + end + + end +end diff --git a/lib/progg/interpret/interpret.rb b/lib/progg/interpret/interpret.rb new file mode 100644 index 0000000..2ee1470 --- /dev/null +++ b/lib/progg/interpret/interpret.rb @@ -0,0 +1,12 @@ +# Require all module files +Dir[File.join(__dir__, "**", '*.rb')].sort.each { |file| require file } + +module Progg + + module Interpret + + class InterpretError < Progg::Core::Error; end + + end + +end diff --git a/lib/progg/interpret/progg_script.rb b/lib/progg/interpret/progg_script.rb new file mode 100644 index 0000000..0d11fc6 --- /dev/null +++ b/lib/progg/interpret/progg_script.rb @@ -0,0 +1,33 @@ + +module Progg + module Interpret + + class ProggScript + + # List of components for this graph + attr_accessor :components + + def initialize() + @components = [] + end + + def interpret(file) + file = File.expand_path(file) + graph_ctx = Interpret::GraphContext.new + Dir.chdir(File.dirname(file)) { eval(File.read(file), graph_ctx.get_binding(), file) } + return graph_ctx.to_model() + end + + def find_component(comp_name) + @components.detect { |s| s.name == comp_name } + end + + def find_component!(comp_name) + component = find_component(comp_name) + raise "No such component '#{comp_name}'" if component.nil? + return component + end + + end + end +end \ No newline at end of file diff --git a/lib/progg/interpret/spec/ltl_builder.rb b/lib/progg/interpret/spec/ltl_builder.rb new file mode 100644 index 0000000..e46cb82 --- /dev/null +++ b/lib/progg/interpret/spec/ltl_builder.rb @@ -0,0 +1,90 @@ +module Progg + module Interpret + + class LTLBuilder + + def globally() + return LTLBuilderGlobally.new() + end + def after(expression) + return LTLBuilderAfter.new(expression) + end + def before(expression) + LTLBuilderBefore.new(expression) + end + def between(); end + def after_until(); end + + class LTLBuilderBase + + def build(pattern, map) + map.each { |key, val| + pattern = pattern.gsub(key.to_s, "#{val}") + } + return pattern + end + + end + + class LTLBuilderGlobally < LTLBuilderBase + def global(p) + build "G p", { p: p } + end + def never(p) + build "G !( p )", { p: p } + end + def exists(p) + build "F p", { p: p } + end + def reacts(p, s) + build "G ( p => F s )", { p: p, s: s } + end + def precedes(p, s) + build "!(p) W s", { p: p, s: s } + end + end + + class LTLBuilderAfter < LTLBuilderBase + attr_accessor :q + def initialize(q); @q = q end + def global(p) + build "G ( q -> G p )", { p: p, q: q } + end + def never(p) + build "G ( q -> G !(p))", { p: p, q: q } + end + def exists(p) + build "( G !(q) ) || ( F ( q && F p ) )", { p: p, q: q } + end + def reacts(p, s) + build "G ( q => G (p => F s) )", { p: p, q: q, s: s} + end + def precedes(p, s) + build "G !(q) || F ( q && !(p) W s )", { p: p, q: q, s: s} + end + end + + class LTLBuilderBefore < LTLBuilderBase + attr_accessor :q + def initialize(q); @q = q end + def global(p) + + end + def never(p) + build "( F q ) => ( !(p) U q )", { p: p, q: q } + end + def exists(p) + + end + def reacts(p, s) + + end + def precedes(p, s) + + end + end + + end + + end +end diff --git a/lib/progg/interpret/spec/spec_context.rb b/lib/progg/interpret/spec/spec_context.rb new file mode 100644 index 0000000..4b879e2 --- /dev/null +++ b/lib/progg/interpret/spec/spec_context.rb @@ -0,0 +1,29 @@ +module Progg + module Interpret + + class SpecContext + # The text of this spec as a string. + attr_accessor :text + + # The LTL/CTL expression of this spec + attr_accessor :expression + + # The parent set of this spec + attr_accessor :parent + + def initialize(text, expression, parent) + @text, @expression, @parent = text, expression, parent + end + + def ltl(expression) + @expression << expression + end + + def to_model(parent) + return Model::Spec.new(@text, @expression, parent) + end + + end + + end +end diff --git a/lib/progg/interpret/spec/spec_set_context.rb b/lib/progg/interpret/spec/spec_set_context.rb new file mode 100644 index 0000000..05a2f66 --- /dev/null +++ b/lib/progg/interpret/spec/spec_set_context.rb @@ -0,0 +1,61 @@ +module Progg + module Interpret + + class SpecSetContext + + # The text of this spec set as a string. + attr_accessor :text + + # The sub-spec sets contained in this spec set + attr_accessor :children + + attr_accessor :parent + + attr_accessor :assumption + + def initialize(text, parent, children = []) + @text, @parent, @children = text, parent, children + end + + def specify(text, &blk) + subset = SpecSetContext.new(text, self) + subset.instance_eval(&blk) + children << subset + end + + def assuming(hash, &blk) + assumption_text = hash.keys.first + assumption_expression = hash.values.first + subset = SpecSetContext.new("", self) + subset.assumption = { text: assumption_text, expression: assumption_expression } + subset.instance_eval(&blk) + children << subset + end + + def it(text_or_hash, &blk) + spec = nil + if text_or_hash.is_a?(Hash) + text = text_or_hash.keys.first + expression = text_or_hash[text] + spec = SpecContext.new(text, expression.to_s, self) + else + spec = SpecContext.new(text, nil, self) + end + spec.instance_eval(&blk) unless blk.nil? + children << spec + end + + def ltl() + return LTLBuilder.new() + end + + def to_model(parent) + model = Model::SpecSet.new(@text, @assumption, parent, []) + model.children = @children.map { |child| child.to_model(model) } + return model + end + + end + end + +end diff --git a/lib/progg/interpret/transition_context.rb b/lib/progg/interpret/transition_context.rb new file mode 100644 index 0000000..a62de9d --- /dev/null +++ b/lib/progg/interpret/transition_context.rb @@ -0,0 +1,44 @@ +module Progg + module Interpret + + class TransitionContext + + # Backreference to the component which owns this transition + attr_accessor :parent_component + + # Source and target states as symbols + attr_accessor :src_state, :tgt_state + + # Lists for the guars, actions and preconditions + attr_accessor :guard_list, :action_list, :precon_list + + def initialize(parent_component, src_state, tgt_state) + @parent_component = parent_component + @src_state, @tgt_state = src_state, tgt_state + @guard_list, @action_list, @precon_list = [], [], [] + end + + def guard(str) + @guard_list << str + end + + def action(str) + action_list << str + end + + def precon(str) + @precon_list << str + end + + def to_model() + guard = @guard_list.empty? ? nil : @guard_list.map { |s| "(#{s})" }.join(' && ') + precon = @precon_list.empty? ? nil : @precon_list.map { |s| "(#{s})" }.join(' && ') + action = @action_list.empty? ? nil : @action_list.join(' | ') + Model::Transition.new(@src_state, @tgt_state, action: action, precon: precon, guard: guard) + end + + + end + + end +end diff --git a/lib/progg/model/action.rb b/lib/progg/model/action.rb new file mode 100644 index 0000000..466533f --- /dev/null +++ b/lib/progg/model/action.rb @@ -0,0 +1,27 @@ +module Progg + module Model + + class Action + + # The expression of this action + attr_accessor :expression + # All resolved variable objects the expression needs + attr_accessor :variables + + def initialize(expression, variables) + @expression, @variables = expression, variables + end + + def calc_illegal_allocations() + @expression.calc_illegal_allocations(@variables) + end + + def to_s() + return @expression.to_s + end + + + end + + end +end \ No newline at end of file diff --git a/lib/progg/model/allocation_set.rb b/lib/progg/model/allocation_set.rb new file mode 100644 index 0000000..5fae406 --- /dev/null +++ b/lib/progg/model/allocation_set.rb @@ -0,0 +1,28 @@ +module Progg + module Model + + class AllocationSet + + # An array of variables + attr_accessor :variables + + # An array of allocations for those variables. + # Each allocation is a an array like [0, 1] where indices match the variable array + # to represent values for that variable + attr_accessor :allocations + + def initialize(variables, allocations) + if !allocations.empty? && variables.length != allocations.first.length + raise "Variables and allocations must match in length!" + end + @variables, @allocations = variables, allocations + end + + def length() + allocations.length + end + + end + + end +end \ No newline at end of file diff --git a/lib/progg/model/assignment.rb b/lib/progg/model/assignment.rb new file mode 100644 index 0000000..8f164f7 --- /dev/null +++ b/lib/progg/model/assignment.rb @@ -0,0 +1,34 @@ + +module Progg + module Model + + class Assignment + + ASSIGN_OPERATOR = ':=' + + # The name of the variable which is assigned a value + attr_accessor :assigned_variable + + # The Model::Expression which of this assignment + attr_accessor :expression + + def self.from_string(string) + raise "Not an assignment: #{string}" unless string.include?(ASSIGN_OPERATOR) + split = string.split(ASSIGN_OPERATOR).map(&:strip) + assigned_variable = split[0].to_sym + expression = Expression.from_string(split[1]) + return Assignment.new(assigned_variable, expression) + end + + def initialize(assigned_variable, expression) + @assigned_variable, @expression = assigned_variable, expression + end + + def to_s() + return "#{assigned_variable} #{ASSIGN_OPERATOR} #{expression.to_s}" + end + + end + + end +end diff --git a/lib/progg/model/component.rb b/lib/progg/model/component.rb new file mode 100644 index 0000000..b3f24df --- /dev/null +++ b/lib/progg/model/component.rb @@ -0,0 +1,36 @@ + +module Progg + module Model + + class Component + + # The name of this component as a symbol + attr_accessor :name + # A list of symbols representing states + attr_accessor :states + # A list of transitions between states + attr_accessor :transitions + + # Variables owned by this component + # attr_accessor :owned_variables + # # Variables which are imported from other components + # attr_accessor :imported_variables + + def initialize(args = {}) + @name = ( args[:name] || raise('Blubb') ) + @states = ( args[:states] || [] ) + @transitions = ( args[:transitions] || [] ) + # @owned_variables = ( args[:owned_variables] || [] ) + # @imported_variables = ( args[:imported_variables] || [] ) + end + + def initial_state() + return states.first + end + + + + end + + end +end \ No newline at end of file diff --git a/lib/progg/model/condition.rb b/lib/progg/model/condition.rb new file mode 100644 index 0000000..59bb4e9 --- /dev/null +++ b/lib/progg/model/condition.rb @@ -0,0 +1,27 @@ +module Progg + module Model + + class Condition + + # The expression of this condition + attr_accessor :expression + + # Resolved Variables objects which the expression uses + attr_accessor :variables + + def initialize(expression, variables) + @expression, @variables = expression, variables + end + + def filter_allocation_set(allocation_set) + @expression.filter_allocation_set(allocation_set) + end + + def to_s() + return @expression.to_s + end + + end + + end +end \ No newline at end of file diff --git a/lib/progg/model/expression.rb b/lib/progg/model/expression.rb new file mode 100644 index 0000000..4982f30 --- /dev/null +++ b/lib/progg/model/expression.rb @@ -0,0 +1,106 @@ +module Progg + module Model + + # Class used to represent a mathematical expression + class Expression + + ASSIGNMENT_OP = ':=' + MAX_ALLOCS_FOR_CHECK = 1000000 + + # 3 * Position + x + # >= 4 + + # The entire expression as a string + attr_accessor :expression_string + + def initialize(expression_string) + @expression_string = expression_string + end + + # Finds all variables in the specified this expression + # and returns them as an unique array of symbols ordered by their occource + def used_variables(expression=@expression_string) + expression.scan(/[a-zA-Z_][a-zA-Z0-9_]*/).uniq.map(&:to_sym) + end + + def assigned_variable() + var, expression = isolate_assigned_variable() + return var + end + + def term_variables() + var, expression = isolate_assigned_variable() + return used_variables(expression) + end + + def assignment?() + return !assigned_variable().nil? + end + + # Calcuates an AllocationSet which is populated with all variable allocations + # which lead to an illegal output value for this expressions variable assignment + def calc_illegal_allocations(resolved_variables) + + assigned_var, term = isolate_assigned_variable() + raise("Term '#{self}' is not a variable assignment!") if assigned_var.nil? + term_vars = used_variables(term) + + # Resolve the variables used in this expression to actual variable objects + assigned_var = resolved_variables.detect {|var| var.name == assigned_var } + term_vars = term_vars.map { |varname| resolved_variables.detect { |var| varname == var.name } } + + # Calculate the number of possible allocations, which is the product of the variable range length + num_combinations = term_vars.map(&:range).map(&:count).reduce(&:*) + + # Set an upper limit to not calculate some huge range forever + raise "Search space too large on validation of term '#{self}': #{num_combinations} > #{MAX_ALLOCS_FOR_CHECK}" \ + if num_combinations > MAX_ALLOCS_FOR_CHECK + + # Calculate all combinations of possible variable assignments based on their range + allocations = term_vars.map(&:range).map(&:to_a).reduce(&:product).map(&:flatten) + + # For each combination of variable allocations create an expression by replacing the variable + # with its value in that allocation + illegal_allocations = allocations.reject { |alloc| + values = term_vars.map(&:name).map(&:to_s).zip(alloc).to_h + expression = term.gsub(/#{term_vars.map(&:name).join("|")}/, values) + + resolved_value = eval(expression) + assigned_var.range.include?(resolved_value) + } + + puts "#{illegal_allocations}" + + return AllocationSet.new(term_vars, illegal_allocations) + end + + # Only keeps allocations in the specified allocation set which are possible + # based on this condition + def filter_allocation_set(allocation_set) + # Only keep allocations for which this condition evaluates to true + allocation_set.allocations.select { |alloc| + values = allocation_set.variables.map(&:name).map(&:to_s).zip(alloc).to_h + term = @expression_string.gsub(/#{allocation_set.variables.map(&:name).join("|")}/, values) + result = eval(term) + raise "Expression #{self} for allocation #{alloc} (#{term}) evaluated to #{result} which is not a boolean" \ + unless result == true || result == false + result == true + } + end + + # This method splits off a potential assigned variable and returns the variable + # which is assigned as a symbol and the remaining expression as a string. + def isolate_assigned_variable() + var = used_variables().first + match = @expression_string[/(#{var}\s*#{ASSIGNMENT_OP})/, 1] + return nil, @expression_string if match.nil? + return var, @expression_string.gsub(match, '').strip + end + + def to_s() + @expression_string + end + + end + end +end \ No newline at end of file diff --git a/lib/progg/model/graph.rb b/lib/progg/model/graph.rb new file mode 100644 index 0000000..101f674 --- /dev/null +++ b/lib/progg/model/graph.rb @@ -0,0 +1,45 @@ + +module Progg + module Model + + class Graph + + # All Model::Component's which are part of this graph + attr_accessor :components + + # A Model::VariableSet of all integer variables declared by + # components in this graph + attr_accessor :variables + + attr_accessor :specification + + def initialize(components: [], variables: VariableSet.new(), specification: Specification.empty()) + raise "Not a variable set #{variables}" unless variables.is_a?(VariableSet) + @components, @variables, @specification = components, variables, specification + end + + # Returns a list of state variables for each component in this graph + # Each state variable is named according to the component it represents + # and has a range consisting of the states of that component + def state_variables() + vars = @components.map { |cmp| + Variable.new(cmp.name, cmp.states, cmp.name, initial_value: cmp.initial_state) + } + return VariableSet.new(*vars) + end + + # Returns all variables used in this graph including state variables + def all_variables() + return state_variables() + @variables + end + + def validate() + errors = [] + errors += UnkownVariableValidation.validate(self) + return errors + end + + end + + end +end \ No newline at end of file diff --git a/lib/progg/model/model.rb b/lib/progg/model/model.rb new file mode 100644 index 0000000..d981d97 --- /dev/null +++ b/lib/progg/model/model.rb @@ -0,0 +1,10 @@ +# Require all module files +Dir[File.join(__dir__, "**", '*.rb')].sort.each { |file| require file } + +module Progg + module Model + + # class ValidationError < Progg::Core::Error; end + + end +end \ No newline at end of file diff --git a/lib/progg/model/parsed_expression.rb b/lib/progg/model/parsed_expression.rb new file mode 100644 index 0000000..cc2422c --- /dev/null +++ b/lib/progg/model/parsed_expression.rb @@ -0,0 +1,32 @@ + +module Progg + module Model + + class ParsedExpression + + attr_accessor :expression_string + attr_accessor :type + attr_accessor :ast + + def initialize(expression_string, type) + # result = EbnfParser.parse_expression(expression_string, type: type) + # TODO: Custom error + # raise result.error if result.error?() + + @expression_string = expression_string + # @type = type + # @ast = result.ast + end + + def used_variables() + return expression_string.scan(/[a-zA-Z_][a-zA-Z0-9_]*/).flatten.compact.map(&:to_sym) + end + + def to_s() + @expression_string + end + + end + + end +end \ No newline at end of file diff --git a/lib/progg/model/specs/spec.rb b/lib/progg/model/specs/spec.rb new file mode 100644 index 0000000..94e81b3 --- /dev/null +++ b/lib/progg/model/specs/spec.rb @@ -0,0 +1,41 @@ +module Progg + module Model + + # A single specification and a leave in the tree + class Spec + + # The text of this spec as a string. + attr_accessor :text + + # The LTL/CTL expression of this spec + attr_accessor :expression + + # The parent specification set for this node + attr_accessor :parent + + def initialize(text, expression, parent) + @text, @expression, @parent = text, expression, parent + end + + def parent? + return !@parent.nil? + end + + def linage() + return parents() + [ self ] + end + + def parents() + array = [] + current = self + while(current.parent?) + current = current.parent + array << current + end + return array.reverse() + end + + end + + end +end diff --git a/lib/progg/model/specs/spec_set.rb b/lib/progg/model/specs/spec_set.rb new file mode 100644 index 0000000..6028ffd --- /dev/null +++ b/lib/progg/model/specs/spec_set.rb @@ -0,0 +1,36 @@ +module Progg + module Model + + class SpecSet + + # The text of this spec set as a string. + attr_accessor :text + + attr_accessor :assumption + + # The sub-spec sets contained in this spec set + attr_accessor :children + + attr_accessor :parent + + def initialize(text, assumption, parent, children) + @text, @assumption, @parent, @children = text, assumption, parent, children + end + + def parent? + return !@parent.nil? + end + + def get_specs() + ret = [] + children.each { |child| + ret << child if child.is_a?(Spec) + ret += child.get_specs() if child.is_a?(SpecSet) + } + return ret + end + + end + + end +end diff --git a/lib/progg/model/specs/specification.rb b/lib/progg/model/specs/specification.rb new file mode 100644 index 0000000..df13f30 --- /dev/null +++ b/lib/progg/model/specs/specification.rb @@ -0,0 +1,53 @@ +module Progg + module Model + + class Specification + + attr_accessor :spec_sets + + def self.empty() + return self.new([]) + end + + def initialize(spec_sets) + @spec_sets = spec_sets + end + + def get_specs() + spec_sets.map(&:get_specs).flatten + end + + def flat_specs() + specs = get_specs() + specs.each { |spec| + parents = spec.parents + prefix = parents.map { |spec_set| + if (spec_set.assumption.nil?) + spec_set.text + else + "assuming #{spec_set.assumption[:text]}".c_sidenote + end + }.join(" ") + text = "#{prefix} #{spec.text}" + + assumption_expression = parents.map { |spec_set| + next if spec_set.assumption.nil? + spec_set.assumption[:expression] + }.compact.join(" && ") + + expression = assumption_expression.empty? \ + ? spec.expression \ + : "( #{assumption_expression} ) => #{spec.expression}" + + + puts "[ #{'PASSED'.c_success} ] " + text + puts " " + expression.c_blue + puts + } + puts "=> [ #{specs.length}/#{specs.length} ] specifications are valid!".c_success + end + + end + + end +end diff --git a/lib/progg/model/transition.rb b/lib/progg/model/transition.rb new file mode 100644 index 0000000..b540ea0 --- /dev/null +++ b/lib/progg/model/transition.rb @@ -0,0 +1,34 @@ +module Progg + module Model + + class Transition + + # The source and target state of this transition as symbols + attr_accessor :src_state, :tgt_state + + attr_accessor :guard, :precon, :action + + def initialize(src_state, tgt_state, guard: "", action: "", precon: "") + @src_state, @tgt_state = src_state, tgt_state + @guard = guard.nil? ? nil : ParsedExpression.new(guard, :Guard) + @action = action.nil? ? nil : ParsedExpression.new(action, :Action) + @precon = precon.nil? ? nil : ParsedExpression.new(precon, :Precon) + end + + def validate!() + # @actions.each { |action| + # # Calculate all illegal allocations + # # An allocation is illegal if it evaluates to a number outside of the range + # # of the assigned variable + # illegal_allocations = action.calc_illegal_allocations() + # # Only keep allocations as illegal if guards do not prevent them + # illegal_allocations = precon.filter_allocation_set(illegal_allocations) + + # raise("ValidationError") if illegal_allocations.length != 0 + # } + end + + end + + end +end diff --git a/lib/progg/model/validations/unkown_variables_validation.rb b/lib/progg/model/validations/unkown_variables_validation.rb new file mode 100644 index 0000000..d9210e9 --- /dev/null +++ b/lib/progg/model/validations/unkown_variables_validation.rb @@ -0,0 +1,56 @@ +require_relative 'validation_error.rb' + +module Progg + module Model + + module UnkownVariableValidation + + class UnkownVariableError < ValidationError + + def initialize(variables, component, transition, variable, expression, type) + @variables, @component, @transition, @variable = variables, component, transition, variable + @expression, @type = expression, type + end + + def title() + return "Unknown variable: '#{@variable}'!" + end + + def body() + trans_s = "(#{@transition.src_state} -> #{@transition.tgt_state})".c_trans + expression = @expression.to_s.gsub(@variable.to_s, @variable.to_s.c_warn) + return "The #{@type} defined in transition #{trans_s} of component #{@component.name.to_s.c_cmp}" \ + " uses variable #{@variable.to_s.c_warn} which could not be found." \ + "\n Expression: #{expression}" \ + "\n Variables: #{@variables.to_s}" + end + + end + + def self.validate(graph) + errors = [] + variables = graph.all_variables() + constants = graph.state_variables().values() + graph.components.each { |component| + component.transitions.each { |transition| + transition.guard&.used_variables()&.uniq&.each { |variable| + next if variables.include?(variable) || constants.include?(variable) + errors << UnkownVariableError.new(variables, component, transition, variable, transition.guard, "guard") + } + transition.precon&.used_variables()&.uniq&.each { |variable| + next if variables.include?(variable) || constants.include?(variable) + errors << UnkownVariableError.new(variables, component, transition, variable, transition.precon, "precondition") + } + transition.action&.used_variables()&.uniq&.each { |variable| + next if variables.include?(variable) || constants.include?(variable) + errors << UnkownVariableError.new(variables, component, transition, variable, transition.action, "action") + } + } + } + return errors + end + + end + + end +end \ No newline at end of file diff --git a/lib/progg/model/validations/validation_error.rb b/lib/progg/model/validations/validation_error.rb new file mode 100644 index 0000000..423f72e --- /dev/null +++ b/lib/progg/model/validations/validation_error.rb @@ -0,0 +1,14 @@ + +module Progg + module Model + + class ValidationError + + def to_s() + return "#{self.title().c_error}\n#{self.body().indented(str: '>> '.c_error)}" + end + + end + + end +end \ No newline at end of file diff --git a/lib/progg/model/variable.rb b/lib/progg/model/variable.rb new file mode 100644 index 0000000..238f9fb --- /dev/null +++ b/lib/progg/model/variable.rb @@ -0,0 +1,42 @@ +module Progg + module Model + + class Variable + + # Name of this variable as a symbol + attr_accessor :name + + # The name of the component which owns this variable as a symbol + attr_accessor :owner_name + + # Range of this variable. This can either be a range like (0..2) + # an array of numbers like [0, 1, 2] or an array of symbols representing + # states of components like [:Idle, :Breaking] + attr_accessor :range + + # Initial value of the variable as an integer + # Can be nil to not provide a fixed initial value + attr_accessor :initial_value + + def initialize(name, range, owner_name, initial_value: nil) + @name, @range, @owner_name, @initial_value = name, range, owner_name, initial_value + end + + # Returns the type of this variable which can either be :int + # for integer variable or :state for state variables + def type() + return @range.first.is_a?(Integer) ? :int : :state + end + + # Returns all possible values of this variable as an array + def values() + return @range if type() == :state + return @range.to_a + end + + + end + + end + +end \ No newline at end of file diff --git a/lib/progg/model/variable_set.rb b/lib/progg/model/variable_set.rb new file mode 100644 index 0000000..f265784 --- /dev/null +++ b/lib/progg/model/variable_set.rb @@ -0,0 +1,80 @@ + +module Progg + module Model + + class VariableSet + + attr_accessor :map + + def initialize(*variables) + @map = {} + self << variables + end + + def <<(var) + return @map[var.name] = var if var.is_a?(Variable) + return var.map { |v| self << v } if var.is_a?(Array) + raise "Not a variable '#{var}'" + end + + def get(*names) + return names.map { |n| self[n] } + end + + def +(varset) + raise "Not a variable set '#{varset}'" unless varset.is_a?(VariableSet) + return VariableSet.new(*(self.to_a() + varset.to_a())) + end + + def to_a() + return @map.values() + end + + def names() + return @map.keys() + end + + def [](name) + raise "No such variable #{name}!" unless @map.key?(name) + return @map[key] + end + + def include?(name_or_var) + return varname?(name_or_var) || constname?(name_or_var) + end + + def empty?() + return @map.empty? + end + + def map(&blk) + return @map.values.map(&blk) + end + + def varname?(name) + return @map.key?(name) + end + + def constname?(name) + @map.values.include?(name) + end + + def to_s() + return "{#{@map.map { |name, var| "#{name}:#{var.range}(#{var.owner_name})" }.join(", ")}}" + end + + def select_by_owner(owner_name) + found = self.to_a().select { |var| var.owner_name == owner_name } + return VariableSet.new(*found) + end + + # Returns all possible values of variables in this set as an array + def values() + return self.to_a().map(&:values).flatten + end + + end + + end +end + \ No newline at end of file diff --git a/lib/progg/nusmv/nusmv.rb b/lib/progg/nusmv/nusmv.rb new file mode 100644 index 0000000..45484ee --- /dev/null +++ b/lib/progg/nusmv/nusmv.rb @@ -0,0 +1,7 @@ +# Require all module files +Dir[File.join(__dir__, "**", '*.rb')].sort.each { |file| require file } + +module Progg + module NuSMV + end +end \ No newline at end of file diff --git a/lib/progg/nusmv/nusmv_runner.rb b/lib/progg/nusmv/nusmv_runner.rb new file mode 100644 index 0000000..b36c289 --- /dev/null +++ b/lib/progg/nusmv/nusmv_runner.rb @@ -0,0 +1,17 @@ + +module Progg + module NuSMV + + class NuSMVRunner + + def initialize() + end + + def load_file(file) + puts `#{Settings.numsv.path} #{file}` + end + + end + + end +end diff --git a/lib/progg/transform/nusmv_transformation.rb b/lib/progg/transform/nusmv_transformation.rb new file mode 100644 index 0000000..08eddb6 --- /dev/null +++ b/lib/progg/transform/nusmv_transformation.rb @@ -0,0 +1,167 @@ + + +module Progg + module Tranform + + class NuSmvTransformation + + def transform_graph(programm_graph) + variables = programm_graph.all_variables + components = programm_graph.components + + var_s = transform_variables(variables) + cmp_s = transform_components(components, variables) + main_s = transform_main_module(components) + return "#{var_s}\n\n#{cmp_s}\n\n#{main_s}" + end + + def transform_variables(varset) + vars_s = varset.to_a.map { |v| transform_variable(v) }.join("\n") + return module_string("_VARS", var: vars_s) + end + + def transform_components(components, varset) + return components.map { |c| transform_component(c, varset) }.join("\n\n") + end + + def transform_variable(variable) + return "#{transform_varname(variable.name)} : #{transform_range(variable.range)}" + end + + def transform_range(range) + # Transform state variables + return "{#{range.map { |e| transform_const(e) }.join(", ")}};" if range.is_a?(Array) + # Transform small integer variables + return "{#{range.join(", ")}};" if (range.last - range.first) < 5 + # Transform regular integer variables + return "#{range.first}..#{range.last};" + end + + def transform_component(component, varset) + # Name of the component module + name = transform_module_name(component.name) + # The component takes all variables v + name += "(v)" + + # Generate the INIT block. Each component initializes it's own variables + cmp_vars = varset.select_by_owner(component.name).to_a + init = cmp_vars.map { |var| + # Allow variables to omit the initital value as to choose an indeterministic value + next if var.initial_value.nil? + "v.#{transform_varname(var.name)} = #{transform_const(var.initial_value)}" + }.compact.join(" & ") + + trans = component.transitions.map { |transition| + trans_s = transform_transition(varset, component, transition) + "( #{trans_s} )" + }.join(" | \n") + trans += ";" + + return module_string(name, init: init, trans: trans) + end + + def transform_transition(varset, component, transition) + expression = [] + + cmp_varname = transform_varname(component.name) + prev_state = transform_const(transition.src_state) + expression << "v.#{cmp_varname} = #{prev_state}" + + next_state = transform_const(transition.tgt_state) + expression << "next(v.#{cmp_varname}) = #{next_state}" + + precon_s = transform_expression(transition.precon, varset) + guard_s = transform_expression(transition.guard, varset) + action_s = transform_expression(transition.action, varset) + expression << precon_s + expression << guard_s + expression << action_s + + # TODO: Actions, preconditions and guards + # ( v.V_UmgebungPosition = L_Moving & next(v.V_UmgebungPosition) = L_Moving & ((v.V_Position < 90) & (v.V_Position < 90)) & (next(v.V_Position) = (v.V_Position + v.V_Speed))) | + # ( v.V_FailureSensor = L_No & next(v.V_FailureSensor) = L_Yes & TRUE & (TRUE)) | + return expression.compact.join(' & ') + end + + def transform_assignment() + "Position := Velocity * Speed" + "next(v.V_Position) = ()" + + + end + + def transform_expression(expression, varset) + return nil if expression.nil? + + expression_s = expression.to_s + + expression_s = expression_s.gsub(/(\w+)\s*:=/) { + assigned_var = Regexp.last_match[1] + "next(#{assigned_var}) =" + } + + expression.used_variables.uniq.each { |symbol| + + symbol_s = varset.varname?(symbol) \ + ? "v.#{transform_varname(symbol)}" \ + : transform_const(symbol) + puts "REPL #{symbol} by #{symbol_s} in '#{expression}'" + + + expression_s = expression_s.gsub(/\bword\b(?!\w)/, symbol_s) { |match| + puts "MATCH: '#{match}'" + } + } + + expression_s = expression_s.gsub('&&', '&') + expression_s = expression_s.gsub('||', '|') + expression_s = expression_s.gsub('||', '|') + expression_s = expression_s.gsub('==', '=') + + + return expression_s + end + + + def transform_main_module(components) + # Instantiate variable module as v + var_s = "v : _VARS();\n" + # Instantiate all component modules, passing in v + var_s += components.map { |component| + instance = transform_module_instance_name(component.name) + modul = transform_module_name(component.name) + "#{instance} : #{modul}(v);" + }.join("\n") + return module_string("main", var: var_s) + end + + def module_string(name, hash = {}) + blocks = [ "MODULE #{name}" ] + hash.each { |key, val| + blocks << key.to_s.upcase.indented + blocks << val.indented(num: 2) + } + return blocks.join("\n") + end + + def transform_varname(name) + "V_#{name}" + end + + def transform_const(value) + return value.to_s unless value.is_a?(Symbol) || value.is_a?(String) + "L_#{value}" + end + + def transform_module_name(name) + "_P_#{name}" + end + + def transform_module_instance_name(name) + "p_#{name}" + end + + end + + end +end diff --git a/lib/progg/transform/puml_transformation.rb b/lib/progg/transform/puml_transformation.rb new file mode 100644 index 0000000..e39cf20 --- /dev/null +++ b/lib/progg/transform/puml_transformation.rb @@ -0,0 +1,85 @@ + + +module Progg + module Tranform + + class PumlTransformation + + def transform_graph(graph) + str = graph.components.map { |c| transform_component(graph, c) }.join("\n\n") + # str += "\n#{transform_import_dependencies(programm_graph.components)}" + + # skinparam defaultFontName Helvetica + return "@startuml Programmgraph\n#{str}\n@enduml" + end + + # def transform_import_dependencies(components) + # dep_map = components.map { |c| [c.name, c.imported_variables.map(&:component_name).uniq] }.uniq + # return dep_map.map { |c, deps| deps.map { |d| "#{c} ..> #{d}" }}.flatten.join("\n") + # end + + def transform_component(graph, component) + # Transform component states + states_s = component.states.map { |s| transform_state(s) }.join("\n") + # Transform component transitions + trans_s = component.transitions.map { |t| transform_transition(t) }.join("\n") + # Transform component variables + vars = graph.variables.select_by_owner(component.name) + vars_s = transform_variables(component, vars) + # Transform the initial state + initial_s = transform_initial(graph, component) + + str = [ states_s, trans_s, vars_s, initial_s ].compact.join("\n") + return "rectangle #{component.name} {\n#{indented(str)}\n}" + end + + def transform_initial(graph, component) + initial_state_name = "#{component.name}Initial" + str = "circle #{initial_state_name}\n" + str += "#{initial_state_name} --> #{component.initial_state}" + + vars = graph.variables.select_by_owner(component.name) + init_var_s = vars.map { |v| + next if v.initial_value.nil? + "#{v.name} == #{v.initial_value}" + }.compact.join(' && ') + + str += ": #{init_var_s}" unless init_var_s.empty? + str += "\n" + return str + end + + def transform_state(state) + return "rectangle #{state}" + end + + def transform_transition(transition) + label = transition.precon.to_s + label += transition.guard.to_s + label += "/ " + transition.action.to_s unless transition.action.nil? + + label = ": #{label}" unless label.strip.empty? + return "#{transition.src_state} --> #{transition.tgt_state} #{label}" + end + + def indented(str) + str.split("\n").map { |s| "\t#{s}" }.join("\n") + end + + def transform_variables(component, variables) + return nil if variables.empty? + body = variables.map { |v| "#{v.name} => #{transform_range(v.range)}" }.join("\n") + return "map #{component.name}Variables {\n#{body}\n}" + end + + def transform_range(range) + return range.to_s if range.is_a?(Range) + return range.map(&:to_s).join(', ') if range.is_a?(Array) + raise "Unknown type for range '#{range}::#{range.class}'" + end + + end + + + end +end \ No newline at end of file diff --git a/lib/progg/transform/transform.rb b/lib/progg/transform/transform.rb new file mode 100644 index 0000000..ed5c4bc --- /dev/null +++ b/lib/progg/transform/transform.rb @@ -0,0 +1,7 @@ +# Require all module files +Dir[File.join(__dir__, "**", '*.rb')].sort.each { |file| require file } + +module Progg + module Tranform + end +end diff --git a/lib/progg/version.rb b/lib/progg/version.rb new file mode 100644 index 0000000..49539eb --- /dev/null +++ b/lib/progg/version.rb @@ -0,0 +1,5 @@ +# frozen_string_literal: true + +module Progg + VERSION = "0.1.0" +end diff --git a/progg.gemspec b/progg.gemspec new file mode 100644 index 0000000..a6979c7 --- /dev/null +++ b/progg.gemspec @@ -0,0 +1,40 @@ +# frozen_string_literal: true + +require_relative "lib/progg/version" + +Gem::Specification.new do |spec| + spec.name = "progg" + spec.version = Progg::VERSION + spec.authors = ["Arian Weber"] + spec.email = ["weber.arian@web.de"] + + spec.summary = "Tool for the decleration and transformation of program graphs" + # spec.description = "TODO: Write a longer description or delete this line." + spec.homepage = "https://github.com/ArianWeber/progg" + spec.required_ruby_version = ">= 2.6.0" + + # spec.metadata["allowed_push_host"] = "TODO: Set to your gem server 'https://example.com'" + + spec.metadata["homepage_uri"] = spec.homepage + # spec.metadata["source_code_uri"] = "TODO: Put your gem's public repo URL here." + # spec.metadata["changelog_uri"] = "TODO: Put your gem's CHANGELOG.md URL here." + + # Specify which files should be added to the gem when it is released. + # The `git ls-files -z` loads the files in the RubyGem that have been added into git. + spec.files = Dir.chdir(__dir__) do + `git ls-files -z`.split("\x0").reject do |f| + (f == __FILE__) || f.match(%r{\A(?:(?:bin|test|spec|features)/|\.(?:git|travis|circleci)|appveyor)}) + end + end + spec.bindir = "exe" + spec.executables = spec.files.grep(%r{\Aexe/}) { |f| File.basename(f) } + spec.require_paths = ["lib"] + + # Gem dependencies + spec.add_dependency "thor", "~> 1.2.1" + spec.add_dependency "ebnf", "~> 2.3.4" + spec.add_dependency "rainbow", "~> 3.0.0" + spec.add_dependency "config", "~> 4.2.1" + spec.add_dependency "plantuml_builder", "~> 0.3.0" + +end diff --git a/sample-project/.gitignore b/sample-project/.gitignore new file mode 100644 index 0000000..e69de29 diff --git a/sample-project/.pg-tools.yml b/sample-project/.pg-tools.yml new file mode 100644 index 0000000..e69de29 diff --git a/sample-project/programm-graph.rb b/sample-project/programm-graph.rb new file mode 100644 index 0000000..e69de29 diff --git a/sig/progg.rbs b/sig/progg.rbs new file mode 100644 index 0000000..1271567 --- /dev/null +++ b/sig/progg.rbs @@ -0,0 +1,4 @@ +module Progg + VERSION: String + # See the writing guide of rbs: https://github.com/ruby/rbs#guides +end diff --git a/spec/lib/progg/ebnf_parser/expression_parser_spec.rb b/spec/lib/progg/ebnf_parser/expression_parser_spec.rb new file mode 100644 index 0000000..e1059ec --- /dev/null +++ b/spec/lib/progg/ebnf_parser/expression_parser_spec.rb @@ -0,0 +1,119 @@ + +RSpec.describe Progg::EbnfParser::ExpressionParser do + + def parser(type: :Expression) + Progg::EbnfParser::ExpressionParser.new(type: type) + end + + INT_ATOMS = [ "1334", "-42", "variable" ] + BOOL_ATOMS = [ "true", "false" ] + ATOMS = (INT_ATOMS + BOOL_ATOMS).uniq + CMP_OPS = [ '<', '>', '<=', '>=', '==' ] + LOGIC_OPS = [ '->', '<->', '', '||', '&&' ] + + context "when evaluating atomic expressions" do + ATOMS.each { |atom| + it "accepts '#{atom}'" do + parser().parse!(atom) + end + } + INT_ATOMS.each { |atom| + it "accepts '#{atom}' as an int expression" do + parser(type: :IntExpr).parse!(atom) + end + } + BOOL_ATOMS.each { |atom| + it "accepts '#{atom}' as a bool expression" do + parser(type: :BoolExpr).parse!(atom) + end + } + INT_ATOMS.each { |atom| + it "rejects '#{atom}' as a bool expression" do + expect { parser(type: :BoolExpr).parse!(atom) }.to raise_error(EBNF::PEG::Parser::Error) + + end + } + BOOL_ATOMS.each { |atom| + it "rejects '#{atom}' as an int expression" do + expect { parser(type: :IntExpr).parse!(atom) }.to raise_error(EBNF::PEG::Parser::Error) + + end + } + end + + context "when using braces" do + INT_ATOMS.each { |atom| + expression = "(#{atom})" + it "accepts '#{expression}' as an int expression" do + parser(type: :IntExpr).parse!(expression) + end + } + BOOL_ATOMS.each { |atom| + expression = "(#{atom})" + it "accepts '#{expression}' as an int expression" do + parser(type: :BoolExpr).parse!(expression) + end + } + end + + context "when evaluating comparison expressions" do + INT_ATOMS.product(INT_ATOMS, CMP_OPS).map(&:flatten).each { |i1, i2, cmp| + expression = "#{i1} #{cmp} #{i2}" + it "accepts '#{expression}'" do + parser().parse!(expression) + end + } + INT_ATOMS.product(BOOL_ATOMS, CMP_OPS).map(&:flatten).each { |i, b, cmp| + next if b == 'variable' + expression = "#{i} #{cmp} #{b}" + it "rejects '#{expression}'" do + expect { parser().parse!(expression) }.to raise_error(EBNF::PEG::Parser::Error) + end + expression = "#{b} #{cmp} #{i}" + it "rejects '#{expression}'" do + expect { parser().parse!(expression) }.to raise_error(EBNF::PEG::Parser::Error) + end + } + end + + context "when evaluating logic expressions" do + BOOL_ATOMS.product(BOOL_ATOMS, LOGIC_OPS).map(&:flatten).each { |b1, b2, cmp| + expression = "#{b2} #{cmp} #{b2}" + it "accepts '#{expression}'" do + parser().parse!(expression) + end + } + end + + context "when evaluating some common expressions" do + + to_accept = { + BoolExpr: [ + "Position + Velocity < 500 && Velocity - Deceleration > 0", + "Velocity - BrakePower > 0", + "(Velocity - BrakePower > 0)", + "((true -> true) && ((false) -> true) ) -> (false -> true)", + "((true -> true) && ((false) -> true) ) -> (false -> true)".gsub("true", "(Position + Velocity < 500 && Velocity - Deceleration > 0)") + ], + IntExpr: [ + "5 + 8 * (X / 15) - 10", + ], + Assignment: [ + "Position := (Position + Velocity)" + ], + Action: [ + "Velocity := Velocity - deceleration | Position := Position + Velocity * 3" + ] + } + + to_accept.each { |type, expressions| + expressions.each { |expression| + it "accepts '#{expression}' as a #{type}" do + parser(type: type).parse!(expression) + end + } + } + + end + +end \ No newline at end of file diff --git a/spec/progg_spec.rb b/spec/progg_spec.rb new file mode 100644 index 0000000..fb99bbb --- /dev/null +++ b/spec/progg_spec.rb @@ -0,0 +1,7 @@ +# frozen_string_literal: true + +RSpec.describe Progg do + it "has a version number" do + expect(Progg::VERSION).not_to be nil + end +end diff --git a/spec/spec_helper.rb b/spec/spec_helper.rb new file mode 100644 index 0000000..06eac2a --- /dev/null +++ b/spec/spec_helper.rb @@ -0,0 +1,15 @@ +# frozen_string_literal: true + +require "progg" + +RSpec.configure do |config| + # Enable flags like --only-failures and --next-failure + config.example_status_persistence_file_path = ".rspec_status" + + # Disable RSpec exposing methods globally on `Module` and `main` + config.disable_monkey_patching! + + config.expect_with :rspec do |c| + c.syntax = :expect + end +end