From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mta1.migadu.com (out-46.mta1.migadu.com [95.215.58.46]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id D935A481666 for ; Wed, 19 Aug 2026 18:16:02 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=95.215.58.46 ARC-Seal:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1787163366; cv=none; b=VY1pU7mf8vj2GyV04kpW4YhBBhmOokY7PqkAHucpJ+Pi724DHcRs9SG7hiXZj0PuwlzLmD7fvqg5oUiQzN06EF7pq8D0AuCwGSxe1Lq3mkiDThNKjlk+5YL+yvMGEqxN4NJjGJBkNopzeqHsRAA+dgfw4qh4iD8NThf80WcDO/E= ARC-Message-Signature:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1787163366; c=relaxed/simple; bh=TmU60pziJvP9jkj9FRe900aTtXpSjdcwaH8P271b+MU=; h=From:To:Cc:Subject:Date:Message-Id:In-Reply-To:References: MIME-Version; b=iNhLEHcwX57UL4mfNGF9GfyZ9Y1FKoBmAl060+p8aVxnvBb25ckJTtgaVmCeLzmSZpZYbPitc+2yEvlaAcdj7tHY28Efhcsm0nj4Ls0Ll5G/kM4Pn5yWmjll23SerowUpr5pIbYMOb7PrgVgYkoNQraZTSDLAZGwi0CftC6JBio= ARC-Authentication-Results:i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linux.dev; spf=pass smtp.mailfrom=linux.dev; dkim=pass (1024-bit key) header.d=linux.dev header.i=@linux.dev header.b=hA9SJpqG; arc=none smtp.client-ip=95.215.58.46 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linux.dev Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=linux.dev Authentication-Results: smtp.subspace.kernel.org; dkim=pass (1024-bit key) header.d=linux.dev header.i=@linux.dev header.b="hA9SJpqG" X-Envelope-To: linux-kernel@vger.kernel.org DKIM-Signature: a=rsa-sha256; bh=TmU60pziJvP9jkj9FRe900aTtXpSjdcwaH8P271b+MU=; c=simple/simple; d=linux.dev; h=from:to:subject:date:message-id:mime-version:content-type; s=key1; t=1787163358; v=1; x=1787768158; b=hA9SJpqGNDv69FVb3FVLKbInfozob+uRtYz6Rh4pEadUzjv2GMR52SrEUdGONFM7UgAyV9VI GjU24EZ3/avHFwmhsvsH4jpEfMKfCoO/MCg61x7uZkQZK/k8KSQtQ7lTOnShcj6nYy6hll5LghL /z0AMl4MrjPalBbIhn6DtEkQ= X-Envelope-To: linux-kernel@vger.kernel.org Received: from localhost.localdomain (180.165.15.98) by mta12.migadu.com with ESMTPS id 561250060a69f1ac; Wed, 19 Aug 2026 18:15:58 +0000 X-Mizu-Trace-ID: 561250060a69f1ac X-Migadu-Flow: FLOW_OUT From: wen.yang@linux.dev To: Gabriele Monaco Cc: Nam Cao , linux-trace-kernel@vger.kernel.org, linux-kernel@vger.kernel.org, Wen Yang Subject: [PATCH v5 3/9] rv: Add tlob model DOT file Date: Thu, 20 Aug 2026 02:15:20 +0800 Message-Id: <306910ca9aa71384ad3bea479a009fd921dc0aae.1787161646.git.wen.yang@linux.dev> X-Mailer: git-send-email 2.25.1 In-Reply-To: References: Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: 8bit From: Wen Yang Add the Graphviz DOT specification of the tlob hybrid automaton to tools/verification/models/. The model has three states (running, waiting, sleeping), five transitions (switch_in, preempt, wakeup, sleep), and a single clock invariant clk_elapsed < BUDGET_NS() active in all states. Suggested-by: Gabriele Monaco Signed-off-by: Wen Yang --- tools/verification/models/tlob.dot | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 tools/verification/models/tlob.dot diff --git a/tools/verification/models/tlob.dot b/tools/verification/models/tlob.dot new file mode 100644 index 000000000000..7f6f09c3d7cf --- /dev/null +++ b/tools/verification/models/tlob.dot @@ -0,0 +1,25 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_stopped"}; + {node [shape = ellipse] "running"}; + {node [shape = plaintext] "running"}; + {node [shape = plaintext] "waiting"}; + {node [shape = plaintext] "sleeping"}; + {node [shape = plaintext] "stopped"}; + "__init_stopped" -> "stopped"; + "running" [label = "running\nclk_elapsed < BUDGET_NS()", color = green3]; + "waiting" [label = "waiting\nclk_elapsed < BUDGET_NS()"]; + "sleeping" [label = "sleeping\nclk_elapsed < BUDGET_NS()"]; + "stopped" [label = "stopped"]; + "running" -> "sleeping" [ label = "sleep" ]; + "running" -> "waiting" [ label = "preempt" ]; + "waiting" -> "running" [ label = "switch_in" ]; + "sleeping" -> "waiting" [ label = "wakeup" ]; + "running" -> "stopped" [ label = "stop" ]; + "stopped" -> "running" [ label = "start;reset(clk_elapsed)" ]; + { rank = min ; + "__init_stopped"; + "stopped"; + } +} -- 2.25.1