An SMT-based bounded model checker for signal temporal logic

Navigation

Verified details

These details have been verified by PyPI
Project links
GitHub Statistics
Maintainers
Avatar for rgyenr2 from gravatar.com rgyenr2

Unverified details

These details have not been verified by PyPI
Project links
Meta
  • License: GPLv3
  • Author: Geunyeol Yu
  • Tags stlmc, model checker, STL, signal temporal logic, bounded model checker
  • Requires: Python >=3.8
Classifiers

Project description

STLmc

STLmc is an SMT-based bounded model checker for signal temporal logic (STL) of hybrid systems. The algorithm of the tool is refutationally complete for STL properties of bounded signals.

For more information about STLmc, please visit our website

Features

  • Bounded model checking
  • Generating trajectories that falsify the given STL properties if any exists
  • Supporting various SMT solvers (e.g., Z3, Yices2, dReal3)

Project details

Verified details

These details have been verified by PyPI
Project links
GitHub Statistics
Maintainers
Avatar for rgyenr2 from gravatar.com rgyenr2

Unverified details

These details have not been verified by PyPI
Project links
Meta
  • License: GPLv3
  • Author: Geunyeol Yu
  • Tags stlmc, model checker, STL, signal temporal logic, bounded model checker
  • Requires: Python >=3.8
Classifiers

Release history Release notifications | RSS feed

This version

1.0.0.dev2 pre-release

1.0.0.dev1 pre-release

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

stlmc-1.0.0.dev2.tar.gz (5.1 MB view details)

Uploaded Source

Built Distributions

stlmc-1.0.0.dev2-cp312-cp312-manylinux_2_5_x86_64.manylinux1_x86_64.whl (4.1 MB view details)

Uploaded CPython 3.12 manylinux: glibc 2.5+ x86-64

stlmc-1.0.0.dev2-cp312-cp312-macosx_14_0_arm64.whl (3.2 MB view details)

Uploaded CPython 3.12 macOS 14.0+ ARM64

stlmc-1.0.0.dev2-cp311-cp311-manylinux_2_5_x86_64.manylinux1_x86_64.whl (4.1 MB view details)

Uploaded CPython 3.11 manylinux: glibc 2.5+ x86-64

stlmc-1.0.0.dev2-cp311-cp311-macosx_14_0_arm64.whl (3.2 MB view details)

Uploaded CPython 3.11 macOS 14.0+ ARM64

stlmc-1.0.0.dev2-cp310-cp310-manylinux_2_5_x86_64.manylinux1_x86_64.whl (4.1 MB view details)

Uploaded CPython 3.10 manylinux: glibc 2.5+ x86-64

stlmc-1.0.0.dev2-cp310-cp310-macosx_14_0_arm64.whl (3.2 MB view details)

Uploaded CPython 3.10 macOS 14.0+ ARM64

stlmc-1.0.0.dev2-cp39-cp39-manylinux_2_5_x86_64.manylinux1_x86_64.whl (4.1 MB view details)

Uploaded CPython 3.9 manylinux: glibc 2.5+ x86-64

stlmc-1.0.0.dev2-cp39-cp39-macosx_14_0_arm64.whl (3.2 MB view details)

Uploaded CPython 3.9 macOS 14.0+ ARM64

stlmc-1.0.0.dev2-cp38-cp38-manylinux_2_5_x86_64.manylinux1_x86_64.whl (4.1 MB view details)

Uploaded CPython 3.8 manylinux: glibc 2.5+ x86-64

stlmc-1.0.0.dev2-cp38-cp38-macosx_14_0_arm64.whl (3.2 MB view details)

Uploaded CPython 3.8 macOS 14.0+ ARM64

File details

Details for the file stlmc-1.0.0.dev2.tar.gz.

File metadata

  • Download URL: stlmc-1.0.0.dev2.tar.gz
  • Upload date:
  • Size: 5.1 MB
  • Tags: Source
  • Uploaded using Trusted Publishing? Yes
  • Uploaded via: twine/5.1.0 CPython/3.12.5

File hashes

Hashes for stlmc-1.0.0.dev2.tar.gz
Algorithm Hash digest
SHA256 a237a4ecd45626e2813b4029afa79cdfd2a87c9a26c3c4f854cf2ca401a80433
MD5 25f8cb3f18d03960e5efb840ec03672f
BLAKE2b-256 009400023810aa28f6ab236022eabae7dfdf995f41132f227d0a7a52929cbc06

See more details on using hashes here.

File details

Details for the file stlmc-1.0.0.dev2-cp312-cp312-manylinux_2_5_x86_64.manylinux1_x86_64.whl.

File metadata

File hashes

Hashes for stlmc-1.0.0.dev2-cp312-cp312-manylinux_2_5_x86_64.manylinux1_x86_64.whl
Algorithm Hash digest
SHA256 dd81d1aecee99497b83b48fbaba17531fc25ff95fabdb1c3d59cd1be1ecd1d8e
MD5 686acfbdd00ac22d2739bdd3fc19676b
BLAKE2b-256 40447b16b83d1554f650bc3a3dec1f17cf6972b75521038cd00ea550c699b2c7

See more details on using hashes here.

File details

Details for the file stlmc-1.0.0.dev2-cp312-cp312-macosx_14_0_arm64.whl.

File metadata

File hashes

Hashes for stlmc-1.0.0.dev2-cp312-cp312-macosx_14_0_arm64.whl
Algorithm Hash digest
SHA256 93fbd5d16587e6e6d4a7a9336291ad691f0020b48a3a8e17ce301bb8eaf12255
MD5 1a119e66696c5cf26eed09e3e5ba11cf
BLAKE2b-256 ba38624b7a37ccef2ecdb7d60b580c8f2f5f35e34b768be7584da4b9781b0f44

See more details on using hashes here.

File details

Details for the file stlmc-1.0.0.dev2-cp311-cp311-manylinux_2_5_x86_64.manylinux1_x86_64.whl.

File metadata

File hashes

Hashes for stlmc-1.0.0.dev2-cp311-cp311-manylinux_2_5_x86_64.manylinux1_x86_64.whl
Algorithm Hash digest
SHA256 0136aa2477a59800dd300f21d8ed1b8cad9e318c4590bfc63803639811b9ac40
MD5 4caf43cf630a06c4b5aee11abc8cde4e
BLAKE2b-256 58f432efb63391ad09b309ad2d345a73367af7fb9fccb581f9fe1e53d725c105

See more details on using hashes here.

File details

Details for the file stlmc-1.0.0.dev2-cp311-cp311-macosx_14_0_arm64.whl.

File metadata

File hashes

Hashes for stlmc-1.0.0.dev2-cp311-cp311-macosx_14_0_arm64.whl
Algorithm Hash digest
SHA256 df4126227297077e834a571c6d8fcd48e590a950ea86b1723668827f222d83d7
MD5 e39097998cfbbd13062c024d36991087
BLAKE2b-256 880bf72414d99e31e92d1e88815d68ab9dedbbfc51ff4ebaf57f0d8a3b6ca391

See more details on using hashes here.

File details

Details for the file stlmc-1.0.0.dev2-cp310-cp310-manylinux_2_5_x86_64.manylinux1_x86_64.whl.

File metadata

File hashes

Hashes for stlmc-1.0.0.dev2-cp310-cp310-manylinux_2_5_x86_64.manylinux1_x86_64.whl
Algorithm Hash digest
SHA256 3d13ab58c5d2958786168e6cc4a6703bf24516ba587bae73cf1d9d6c257bea39
MD5 fa878310af95d1129c509af623a52fa7
BLAKE2b-256 006c193eaf1a096e23e2d3e6f576f569b15cb0bde8e3e4b3742429e127920999

See more details on using hashes here.

File details

Details for the file stlmc-1.0.0.dev2-cp310-cp310-macosx_14_0_arm64.whl.

File metadata

File hashes

Hashes for stlmc-1.0.0.dev2-cp310-cp310-macosx_14_0_arm64.whl
Algorithm Hash digest
SHA256 72cfd617f003bb522774458104422dfca3440a823a1d97a15791283d0007acbc
MD5 beb8556b80e21c6ca43c17735e292747
BLAKE2b-256 4aeee2be441963b6dde747ba64f575cecb2a6a6cd0b7a84416b0c177d9d89add

See more details on using hashes here.

File details

Details for the file stlmc-1.0.0.dev2-cp39-cp39-manylinux_2_5_x86_64.manylinux1_x86_64.whl.

File metadata

File hashes

Hashes for stlmc-1.0.0.dev2-cp39-cp39-manylinux_2_5_x86_64.manylinux1_x86_64.whl
Algorithm Hash digest
SHA256 6b108a5a73374c21b26bf7d333197e9c2a642dc0d5f42b5eee5091d5821cb504
MD5 d9b5bf53b9fadb68ace629cc2b135d63
BLAKE2b-256 6a756c626216b35abee03dcfd1e6ad4954e8ae6ef398e3f1a613a999d7466f5f

See more details on using hashes here.

File details

Details for the file stlmc-1.0.0.dev2-cp39-cp39-macosx_14_0_arm64.whl.

File metadata

File hashes

Hashes for stlmc-1.0.0.dev2-cp39-cp39-macosx_14_0_arm64.whl
Algorithm Hash digest
SHA256 929ca2f9ff75f4aafbe1e066acea418e88a91a25903f9d9228fd7134e6d686ad
MD5 1fd5026eb9a9199b602eec3e89974966
BLAKE2b-256 d886197f50bfabe37b0c7af659e884fb671195dc5b8f407230017b36b1328ad4

See more details on using hashes here.

File details

Details for the file stlmc-1.0.0.dev2-cp38-cp38-manylinux_2_5_x86_64.manylinux1_x86_64.whl.

File metadata

File hashes

Hashes for stlmc-1.0.0.dev2-cp38-cp38-manylinux_2_5_x86_64.manylinux1_x86_64.whl
Algorithm Hash digest
SHA256 12b9fb873e9ce80cbbf2adcaf3a06a65b487107afaafef347b12e0c8e9ee3034
MD5 0d6dd7e39d79750cdc783556e20224ba
BLAKE2b-256 bec4bb4a54a505eaf5c57668990264e3003c0dba4fb3921a9dc14a90df1e55f9

See more details on using hashes here.

File details

Details for the file stlmc-1.0.0.dev2-cp38-cp38-macosx_14_0_arm64.whl.

File metadata

File hashes

Hashes for stlmc-1.0.0.dev2-cp38-cp38-macosx_14_0_arm64.whl
Algorithm Hash digest
SHA256 862a8196e50d0e9a97d2ca29e1d9773ccdc1007ac4af75f3de86c669f260a677
MD5 f4d6dded63046bda7ad8b85ad97624e6
BLAKE2b-256 6dd20e040217e096f6fb2014e0ab14b07de654faaa96341863a8d23a20d6b86b

See more details on using hashes here.

Supported by

AWS AWS Cloud computing and Security Sponsor Datadog Datadog Monitoring Fastly Fastly CDN Google Google Download Analytics Microsoft Microsoft PSF Sponsor Pingdom Pingdom Monitoring Sentry Sentry Error logging StatusPage StatusPage Status page