Skip to content

Instantly share code, notes, and snippets.

@Agnishom
Agnishom / complexity.md
Created May 28, 2024 22:22
Temporal Logic Monitoring Complexity
  • Results from [ThatiR05]
    • Algorithm is referred to as resolving the past and deriving the future
      • involves transforming the formula
    • Metric Temporal Logic with both Past and Future
    • Upperbounds
      • MTL + Past + Future
        • Space: $O(m 2^m)$
        • Time: $O(m^3 2^{3m})$ for processing each event
  • $m$ is size of formula + sum of numercal constants
@Agnishom
Agnishom / Sets.v
Last active April 30, 2024 21:43
Rewriting with Morphisms
Require Export Setoid.
Require Export Relation_Definitions.
Section ASet.
Declare Scope aset_scope.
Delimit Scope aset_scope with aset. (* so that we can write term%aset *)
Open Scope aset_scope.
@Agnishom
Agnishom / Attempt1.v
Last active November 22, 2023 05:20
Convoy Pattern + Sigma Types + Equations
Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Operators.
Require Import Coq.Wellfounded.Lexicographic_Product.
Require Import Coq.Arith.Wf_nat.
Require Import Arith.
Import ListNotations.
Require Import Coq.Init.Nat.
Require Import Lia.
@Agnishom
Agnishom / boostregex-test.cpp
Last active September 14, 2023 18:18
Regex Execution
// g++ -o boostregex-test boostregex-test.cpp -lboost_regex
#include <fstream>
#include <vector>
#include <string>
#include <iostream>
#include <sstream>
#include <iomanip>
#include <chrono>
#include <boost/regex.hpp>
@Agnishom
Agnishom / Recursion.v
Created September 2, 2023 01:23
Non-obvious Recursion
Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Operators.
Require Import Coq.Wellfounded.Lexicographic_Product.
Require Import Coq.Arith.Wf_nat.
Import ListNotations.
Require Import Coq.Init.Nat.
Require Import Lia.
@Agnishom
Agnishom / Recursion.v
Last active September 1, 2023 21:46
Recursion on Two Arguments
Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Operators.
Import ListNotations.
Require Import Coq.Init.Nat.
Require Import Recdef.
Require Import FunInd.
Require Import Coq.Program.Wf.
@Agnishom
Agnishom / RegexParseTreesFull.v
Last active May 13, 2023 07:26
Parse Tree Preference
Require Import Coq.Lists.List.
Declare Scope regex_scope.
Open Scope regex_scope.
Section Regex.
Variable (A : Type).
Inductive Regex : Type :=
@Agnishom
Agnishom / AwesomeListLemmas.v
Last active April 26, 2024 14:20
Awesome List Lemmas
(*
Some lemmas that can be used in conjunction with those in Coq.Lists.List
See https://coq.inria.fr/library/Coq.Lists.List.html
*)
Require Import Lia.
Require Import Coq.Lists.List.
@Agnishom
Agnishom / pcre.cpp
Last active February 24, 2023 22:00
PCRE Execution
#include <iostream>
#include <string>
#include <pcre.h>
#include <chrono>
using namespace std;
int main() {
string pattern;
string input;
@Agnishom
Agnishom / main.rs
Created September 29, 2022 14:34
Paige-Tarjan
use std::collections::VecDeque;
use std::cell::RefCell;
use std::rc::Rc;
use std::cell::Ref;
pub mod vllsimple;
use vllsimple::*;
struct part_man{
// pools